diff options
| author | Jasper Hugunin | 2020-10-08 17:05:41 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-08 17:05:41 -0700 |
| commit | f96047484333b0b3d37b601abb56a51e56522754 (patch) | |
| tree | e9aba2b4a9f166a7641e1c0b0a3611cda695c8b9 | |
| parent | 9a55d469042cef943dd0be20083896741a1c5dcc (diff) | |
Modify Numbers/Integer/Abstract/ZMulOrder.v to compile with -mangle-names
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 7d97d11818..0275a5fa65 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -167,7 +167,7 @@ Qed. Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1. Proof. assert (F := lt_m1_0). -zero_pos_neg n. +intro n; zero_pos_neg n. (* n = 0 *) intros m. nzsimpl. now left. (* 0 < n, proving P n /\ P (-n) *) @@ -205,7 +205,7 @@ Qed. Theorem lt_mul_r : forall n m p, 0 < n -> 1 < p -> n < m -> n < m * p. Proof. -intros. stepl (n * 1) by now rewrite mul_1_r. +intros n m p **. stepl (n * 1) by now rewrite mul_1_r. apply mul_lt_mono_nonneg. now apply lt_le_incl. assumption. apply le_0_1. assumption. Qed. |