diff options
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 0403722cb3..1e66d9b9ef 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -269,7 +269,7 @@ Module ZnZ. case (of_pos p); intros n w1; simpl. case n; simpl Npos; auto with zarith. intros p1 Hp1; contradict Hp; apply Zle_not_lt. - replace (base digits) with (1 * base digits + 0) by auto with zarith. + replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. apply Zplus_le_compat. apply Zmult_le_compat; auto with zarith. diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 0796d9f49b..1149bc2cdd 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -100,7 +100,7 @@ Theorem pred_succ : forall n, P (S n) == n. Proof. intro n. zify. rewrite <- pred_mod_wB. -replace ([| n |] + 1 - 1)%Z with [| n |] by auto with zarith. apply NZ_to_Z_mod. +replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod. Qed. Section Induction. @@ -170,7 +170,7 @@ Theorem sub_succ_r : forall n m, n - (S m) == P (n - m). Proof. intros n m. zify. rewrite Zminus_mod_idemp_r, Zminus_mod_idemp_l. now replace ([|n|] - ([|m|] + 1))%Z with ([|n|] - [|m|] - 1)%Z - by auto with zarith. + by ring. Qed. Theorem mul_0_l : forall n, 0 * n == 0. |