From 0aeb8e1e2224dc46857cd952f0cd241aa7c3c44f Mon Sep 17 00:00:00 2001 From: notin Date: Mon, 18 Feb 2008 15:42:05 +0000 Subject: 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 --- contrib/setoid_ring/Field_theory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index fd5fa1f694..adaa340db3 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). -- cgit v1.2.3