diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/CyclicAxioms.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 |
1 files changed, 1 insertions, 1 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. |