diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-18 15:42:05 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-18 15:42:05 +0000 |
| commit | 0aeb8e1e2224dc46857cd952f0cd241aa7c3c44f (patch) | |
| tree | cc945338969f4baa9e9424d47e2401904a21139d | |
| parent | b4d172b798c6fc96de3bff55c0bdf444905bb6d7 (diff) | |
Petite correction suite à la révision 10571
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10575 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index fd5fa1f69..adaa340db 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -861,7 +861,7 @@ destruct n. (Zpos p1 - Zpos p6 = Zpos p1 - Zpos p4 + (Zpos p4 - Zpos p6))%Z. change ((Zpos p1 - Zpos p6)%Z = (Zpos p1 + (- Zpos p4) + (Zpos p4 +(- Zpos p6)))%Z). rewrite <- Zplus_assoc. rewrite (Zplus_assoc (- Zpos p4)). - simpl. rewrite Pcompare_refl. reflexivity. + simpl. rewrite Pcompare_refl. simpl. reflexivity. unfold Zminus, Zopp in H0. simpl in H0. rewrite H2 in H0;rewrite H4 in H0;rewrite H in H0. inversion H0;trivial. simpl. repeat rewrite pow_th.(rpow_pow_N). |