diff options
Diffstat (limited to 'theories/Numbers')
| -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 17c69d226..3586cb7f2 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -290,7 +290,7 @@ Module ZnZ. intros p Hp. generalize (spec_of_pos p). case (of_pos p); intros n w1; simpl. - case n; simpl Npos; auto with zarith. + case n; auto with zarith. intros p1 Hp1; contradict Hp; apply Z.le_ngt. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. |