Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 345 insertions, 347 deletions

diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index d6c19410f..fecdb294b 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -18,9 +18,9 @@ Section Setoid_rings.
 Variable A : Type.
 Variable Aequiv : A -> A -> Prop.
 
-Infix Local "==" Aequiv (at level 5, no associativity).
+Infix Local "==" := Aequiv (at level 70, no associativity).
 
-Variable S : (Setoid_Theory A Aequiv).
+Variable S : Setoid_Theory A Aequiv.
 
 Add Setoid A Aequiv S.
 
@@ -31,390 +31,388 @@ Variable Azero : A.
 Variable Aopp : A -> A.
 Variable Aeq : A -> A -> bool.
 
-Infix 4 "+" Aplus V8only 50 (left associativity).
-Infix 4 "*" Amult V8only 40 (left associativity).
+Infix "+" := Aplus (at level 50, left associativity).
+Infix "*" := Amult (at level 40, left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- x" := (Aopp x) (at level 0) V8only.
+Notation "- x" := (Aopp x).
 
-Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
-Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.
-Variable opp_morph : (a,a0:A) a == a0 -> -a == -a0.
+Variable
+  plus_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a + a1 == a0 + a2.
+Variable
+  mult_morph : forall a a0 a1 a2:A, a == a0 -> a1 == a2 -> a * a1 == a0 * a2.
+Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0.
 
 Add Morphism Aplus : Aplus_ext.
-Exact plus_morph.
-Save.
+exact plus_morph.
+Qed.
 
 Add Morphism Amult : Amult_ext.
-Exact mult_morph.
-Save.
+exact mult_morph.
+Qed.
 
 Add Morphism Aopp : Aopp_ext.
-Exact opp_morph.
-Save.
+exact opp_morph.
+Qed.
 
 Section Theory_of_semi_setoid_rings.
 
-Record Semi_Setoid_Ring_Theory : Prop :=
-{ SSR_plus_sym  : (n,m:A) n + m == m + n;
-  SSR_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
-  SSR_mult_sym : (n,m:A) n*m == m*n;
-  SSR_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
-  SSR_plus_zero_left :(n:A) 0 + n == n;
-  SSR_mult_one_left : (n:A) 1*n == n;
-  SSR_mult_zero_left : (n:A) 0*n == 0;
-  SSR_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p;
-  SSR_plus_reg_left : (n,m,p:A)n + m == n + p -> m == p;
-  SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y
-}.
+Record Semi_Setoid_Ring_Theory : Prop := 
+  {SSR_plus_comm : forall n m:A, n + m == m + n;
+   SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
+   SSR_mult_comm : forall n m:A, n * m == m * n;
+   SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
+   SSR_plus_zero_left : forall n:A, 0 + n == n;
+   SSR_mult_one_left : forall n:A, 1 * n == n;
+   SSR_mult_zero_left : forall n:A, 0 * n == 0;
+   SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
+   SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p;
+   SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.
 
 Variable T : Semi_Setoid_Ring_Theory.
 
-Local plus_sym  := (SSR_plus_sym T).
-Local plus_assoc := (SSR_plus_assoc T).
-Local mult_sym  := ( SSR_mult_sym T).
-Local mult_assoc := (SSR_mult_assoc T).
-Local plus_zero_left := (SSR_plus_zero_left T).
-Local mult_one_left := (SSR_mult_one_left T). 
-Local mult_zero_left := (SSR_mult_zero_left T).
-Local distr_left := (SSR_distr_left T).
-Local plus_reg_left := (SSR_plus_reg_left T).
-Local equiv_refl := (Seq_refl A Aequiv S).
-Local equiv_sym := (Seq_sym A Aequiv S).
-Local equiv_trans := (Seq_trans A Aequiv S).
-
-Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
-  plus_zero_left mult_one_left mult_zero_left distr_left
-  plus_reg_left equiv_refl (*equiv_sym*).
-Hints Immediate equiv_sym.
+Let plus_comm := SSR_plus_comm T.
+Let plus_assoc := SSR_plus_assoc T.
+Let mult_comm := SSR_mult_comm T.
+Let mult_assoc := SSR_mult_assoc T.
+Let plus_zero_left := SSR_plus_zero_left T.
+Let mult_one_left := SSR_mult_one_left T. 
+Let mult_zero_left := SSR_mult_zero_left T.
+Let distr_left := SSR_distr_left T.
+Let plus_reg_left := SSR_plus_reg_left T.
+Let equiv_refl := Seq_refl A Aequiv S.
+Let equiv_sym := Seq_sym A Aequiv S.
+Let equiv_trans := Seq_trans A Aequiv S.
+
+Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
+  mult_one_left mult_zero_left distr_left plus_reg_left
+  equiv_refl (*equiv_sym*).
+Hint Immediate equiv_sym.
 
 (* Lemmas whose form is x=y are also provided in form y=x because
   Auto does not symmetry *) 
-Lemma SSR_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
-Auto. Save.
-
-Lemma SSR_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
-Auto. Save.
-
-Lemma SSR_plus_zero_left2 : (n:A) n == 0 + n.
-Auto. Save.
-
-Lemma SSR_mult_one_left2 : (n:A) n == 1*n.
-Auto. Save.
-
-Lemma SSR_mult_zero_left2 : (n:A) 0 == 0*n.
-Auto. Save.
-
-Lemma SSR_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
-Auto. Save.
-
-Lemma SSR_plus_permute : (n,m,p:A) n+(m+p) == m+(n+p).
-Intros.
-Rewrite (plus_assoc n m p).
-Rewrite (plus_sym n m).
-Rewrite <- (plus_assoc m n p).
-Trivial.
-Save.
-
-Lemma SSR_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
-Intros.
-Rewrite (mult_assoc n m p).
-Rewrite (mult_sym n m).
-Rewrite <- (mult_assoc m n p).
-Trivial.
-Save.
-
-Hints Resolve SSR_plus_permute SSR_mult_permute.
-
-Lemma SSR_distr_right : (n,m,p:A) n*(m+p) == (n*m) + (n*p).
-Intros.
-Rewrite (mult_sym n (Aplus m p)).
-Rewrite (mult_sym n m).
-Rewrite (mult_sym n p).
-Auto.
-Save.
-
-Lemma SSR_distr_right2 : (n,m,p:A) (n*m) + (n*p) == n*(m + p).
-Intros.
-Apply equiv_sym.
-Apply SSR_distr_right.
-Save.
-
-Lemma SSR_mult_zero_right : (n:A) n*0 == 0.
-Intro; Rewrite (mult_sym n Azero); Auto.
-Save.
-
-Lemma SSR_mult_zero_right2 : (n:A) 0 == n*0.
-Intro; Rewrite (mult_sym n Azero); Auto.
-Save.
-
-Lemma SSR_plus_zero_right :(n:A) n + 0 == n.
-Intro; Rewrite (plus_sym n Azero); Auto.
-Save.
-
-Lemma SSR_plus_zero_right2 :(n:A) n == n + 0.
-Intro; Rewrite (plus_sym n Azero); Auto.
-Save.
-
-Lemma SSR_mult_one_right : (n:A) n*1 == n.
-Intro; Rewrite (mult_sym n Aone); Auto.
-Save.
-
-Lemma SSR_mult_one_right2 : (n:A) n == n*1.
-Intro; Rewrite (mult_sym n Aone); Auto.
-Save.
-
-Lemma SSR_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p.
-Intros n m p; Rewrite (plus_sym m n); Rewrite (plus_sym p n).
-Intro; Apply plus_reg_left with n; Trivial.
-Save.
+Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).
+auto. Qed.
+
+Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).
+auto. Qed.
+
+Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n.
+auto. Qed.
+
+Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n.
+auto. Qed.
+
+Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n.
+auto. Qed.
+
+Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.
+auto. Qed.
+
+Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).
+intros.
+rewrite (plus_assoc n m p).
+rewrite (plus_comm n m).
+rewrite <- (plus_assoc m n p).
+trivial.
+Qed.
+
+Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).
+intros.
+rewrite (mult_assoc n m p).
+rewrite (mult_comm n m).
+rewrite <- (mult_assoc m n p).
+trivial.
+Qed.
+
+Hint Resolve SSR_plus_permute SSR_mult_permute.
+
+Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.
+intros.
+rewrite (mult_comm n (m + p)).
+rewrite (mult_comm n m).
+rewrite (mult_comm n p).
+auto.
+Qed.
+
+Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).
+intros.
+apply equiv_sym.
+apply SSR_distr_right.
+Qed.
+
+Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0.
+intro; rewrite (mult_comm n 0); auto.
+Qed.
+
+Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0.
+intro; rewrite (mult_comm n 0); auto.
+Qed.
+
+Lemma SSR_plus_zero_right : forall n:A, n + 0 == n.
+intro; rewrite (plus_comm n 0); auto.
+Qed.
+
+Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0.
+intro; rewrite (plus_comm n 0); auto.
+Qed.
+
+Lemma SSR_mult_one_right : forall n:A, n * 1 == n.
+intro; rewrite (mult_comm n 1); auto.
+Qed.
+
+Lemma SSR_mult_one_right2 : forall n:A, n == n * 1.
+intro; rewrite (mult_comm n 1); auto.
+Qed.
+
+Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.
+intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n).
+intro; apply plus_reg_left with n; trivial.
+Qed.
 
 End Theory_of_semi_setoid_rings.
 
 Section Theory_of_setoid_rings.
 
-Record Setoid_Ring_Theory : Prop :=
-{ STh_plus_sym  : (n,m:A) n + m == m + n;
-  STh_plus_assoc : (n,m,p:A) n + (m + p) == (n + m) + p;
-  STh_mult_sym : (n,m:A) n*m == m*n;
-  STh_mult_assoc : (n,m,p:A) n*(m*p) == (n*m)*p;
-  STh_plus_zero_left :(n:A) 0 + n == n;
-  STh_mult_one_left : (n:A) 1*n == n;
-  STh_opp_def : (n:A)  n + (-n) == 0;
-  STh_distr_left : (n,m,p:A) (n + m)*p == n*p + m*p;
-  STh_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x == y
-}.
+Record Setoid_Ring_Theory : Prop := 
+  {STh_plus_comm : forall n m:A, n + m == m + n;
+   STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
+   STh_mult_sym : forall n m:A, n * m == m * n;
+   STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
+   STh_plus_zero_left : forall n:A, 0 + n == n;
+   STh_mult_one_left : forall n:A, 1 * n == n;
+   STh_opp_def : forall n:A, n + - n == 0;
+   STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
+   STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.
 
 Variable T : Setoid_Ring_Theory.
 
-Local plus_sym  := (STh_plus_sym T).
-Local plus_assoc := (STh_plus_assoc T).
-Local mult_sym  := (STh_mult_sym T).
-Local mult_assoc := (STh_mult_assoc T).
-Local plus_zero_left := (STh_plus_zero_left T).
-Local mult_one_left := (STh_mult_one_left T). 
-Local opp_def := (STh_opp_def T).
-Local distr_left := (STh_distr_left T).
-Local equiv_refl := (Seq_refl A Aequiv S).
-Local equiv_sym := (Seq_sym A Aequiv S).
-Local equiv_trans := (Seq_trans A Aequiv S).
-
-Hints Resolve plus_sym plus_assoc mult_sym mult_assoc
-  plus_zero_left mult_one_left opp_def distr_left
-  equiv_refl equiv_sym.
+Let plus_comm := STh_plus_comm T.
+Let plus_assoc := STh_plus_assoc T.
+Let mult_comm := STh_mult_sym T.
+Let mult_assoc := STh_mult_assoc T.
+Let plus_zero_left := STh_plus_zero_left T.
+Let mult_one_left := STh_mult_one_left T. 
+Let opp_def := STh_opp_def T.
+Let distr_left := STh_distr_left T.
+Let equiv_refl := Seq_refl A Aequiv S.
+Let equiv_sym := Seq_sym A Aequiv S.
+Let equiv_trans := Seq_trans A Aequiv S.
+
+Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
+  mult_one_left opp_def distr_left equiv_refl equiv_sym.
 
 (* Lemmas whose form is x=y are also provided in form y=x because Auto does
   not symmetry *)
 
-Lemma STh_mult_assoc2 : (n,m,p:A) (n * m) * p == n * (m * p).
-Auto. Save.
-
-Lemma STh_plus_assoc2 : (n,m,p:A) (n + m) + p == n + (m + p).
-Auto. Save.
-
-Lemma STh_plus_zero_left2 : (n:A) n == 0 + n.
-Auto. Save.
-
-Lemma STh_mult_one_left2 : (n:A) n == 1*n.
-Auto. Save.
-
-Lemma STh_distr_left2 : (n,m,p:A) n*p + m*p  == (n + m)*p.
-Auto. Save.
-
-Lemma STh_opp_def2 : (n:A) 0 == n + (-n).
-Auto. Save.
-
-Lemma STh_plus_permute : (n,m,p:A) n + (m + p) == m + (n + p).
-Intros.
-Rewrite (plus_assoc n m p).
-Rewrite (plus_sym n m).
-Rewrite <- (plus_assoc m n p).
-Trivial.
-Save.
-
-Lemma STh_mult_permute : (n,m,p:A) n*(m*p) == m*(n*p).
-Intros.
-Rewrite (mult_assoc n m p).
-Rewrite (mult_sym n m).
-Rewrite <- (mult_assoc m n p).
-Trivial.
-Save.
-
-Hints Resolve STh_plus_permute STh_mult_permute.
-
-Lemma Saux1 : (a:A)  a + a == a -> a == 0.
-Intros.
-Rewrite <- (plus_zero_left a).
-Rewrite (plus_sym Azero a).
-Setoid_replace (Aplus a Azero) with (Aplus a (Aplus a (Aopp a))); Auto.
-Rewrite (plus_assoc a a (Aopp a)).
-Rewrite H.
-Apply opp_def.
-Save.
-
-Lemma STh_mult_zero_left :(n:A) 0*n == 0.
-Intros.
-Apply Saux1.
-Rewrite <- (distr_left Azero Azero n).
-Rewrite (plus_zero_left Azero).
-Trivial.
-Save.
-Hints Resolve STh_mult_zero_left.
-
-Lemma STh_mult_zero_left2 : (n:A) 0 == 0*n.
-Auto.
-Save.
-
-Lemma Saux2 : (x,y,z:A) x+y==0 -> x+z==0 -> y == z.
-Intros.
-Rewrite <- (plus_zero_left y).
-Rewrite <- H0.
-Rewrite <- (plus_assoc x z y).
-Rewrite (plus_sym z y).
-Rewrite (plus_assoc x y z).
-Rewrite H.
-Auto.
-Save.
-
-Lemma STh_opp_mult_left : (x,y:A) -(x*y) == (-x)*y.
-Intros.
-Apply Saux2 with (Amult x y); Auto.
-Rewrite <- (distr_left x (Aopp x) y).
-Rewrite (opp_def x).
-Auto.
-Save.
-Hints Resolve STh_opp_mult_left.
-
-Lemma STh_opp_mult_left2 : (x,y:A) (-x)*y == -(x*y) .
-Auto.
-Save.
-
-Lemma STh_mult_zero_right : (n:A) n*0 == 0.
-Intro; Rewrite (mult_sym n Azero); Auto.
-Save.
-
-Lemma STh_mult_zero_right2 : (n:A) 0 == n*0.
-Intro; Rewrite (mult_sym n Azero); Auto.
-Save.
-
-Lemma STh_plus_zero_right :(n:A) n + 0 == n.
-Intro; Rewrite (plus_sym n Azero); Auto.
-Save.
-
-Lemma STh_plus_zero_right2 :(n:A) n == n + 0.
-Intro; Rewrite (plus_sym n Azero); Auto.
-Save.
-
-Lemma STh_mult_one_right : (n:A) n*1 == n.
-Intro; Rewrite (mult_sym n Aone); Auto.
-Save.
-
-Lemma STh_mult_one_right2  : (n:A) n == n*1.
-Intro; Rewrite (mult_sym n Aone); Auto.
-Save.
-
-Lemma STh_opp_mult_right : (x,y:A) -(x*y) == x*(-y).
-Intros.
-Rewrite (mult_sym x y).
-Rewrite (mult_sym x (Aopp y)).
-Auto.
-Save.
-
-Lemma STh_opp_mult_right2 : (x,y:A) x*(-y) == -(x*y).
-Intros.
-Rewrite (mult_sym x y).
-Rewrite (mult_sym x (Aopp y)).
-Auto.
-Save.
-
-Lemma STh_plus_opp_opp : (x,y:A) (-x) + (-y) == -(x+y).
-Intros.
-Apply Saux2 with (Aplus x y); Auto.
-Rewrite (STh_plus_permute (Aplus x y) (Aopp x) (Aopp y)).
-Rewrite <- (plus_assoc x y (Aopp y)).
-Rewrite (opp_def y); Rewrite (STh_plus_zero_right x).
-Rewrite (STh_opp_def2 x); Trivial.
-Save.
-
-Lemma STh_plus_permute_opp: (n,m,p:A) (-m)+(n+p) == n+((-m)+p).
-Auto.
-Save.
-
-Lemma STh_opp_opp : (n:A) -(-n) == n.
-Intro.
-Apply Saux2 with (Aopp n); Auto.
-Rewrite (plus_sym (Aopp n) n); Auto.
-Save.
-Hints Resolve STh_opp_opp.
-
-Lemma STh_opp_opp2 : (n:A) n == -(-n).
-Auto.
-Save.
-
-Lemma STh_mult_opp_opp : (x,y:A) (-x)*(-y) == x*y.
-Intros.
-Rewrite (STh_opp_mult_left2 x (Aopp y)).
-Rewrite (STh_opp_mult_right2 x y).
-Trivial.
-Save.
-
-Lemma STh_mult_opp_opp2 : (x,y:A) x*y == (-x)*(-y).
-Intros.
-Apply equiv_sym.
-Apply STh_mult_opp_opp.
-Save.
-
-Lemma STh_opp_zero : -0 == 0.
-Rewrite <- (plus_zero_left (Aopp Azero)).
-Trivial.
-Save.
-
-Lemma STh_plus_reg_left : (n,m,p:A) n+m == n+p -> m==p.
-Intros.
-Rewrite <- (plus_zero_left m).
-Rewrite <- (plus_zero_left p).
-Rewrite <- (opp_def n).
-Rewrite (plus_sym n (Aopp n)).
-Rewrite <- (plus_assoc (Aopp n) n m).
-Rewrite <- (plus_assoc (Aopp n) n p).
-Auto.
-Save.
-
-Lemma STh_plus_reg_right : (n,m,p:A) m+n == p+n -> m==p.
-Intros.
-Apply STh_plus_reg_left with n.
-Rewrite (plus_sym n m); Rewrite (plus_sym n p);
-Assumption.
-Save.
-
-Lemma STh_distr_right : (n,m,p:A) n*(m+p) == (n*m)+(n*p).
-Intros.
-Rewrite (mult_sym n (Aplus m p)).
-Rewrite (mult_sym n m).
-Rewrite (mult_sym n p).
-Trivial.
-Save.
-
-Lemma STh_distr_right2 : (n,m,p:A) (n*m)+(n*p) == n*(m+p).
-Intros.
-Apply equiv_sym.
-Apply STh_distr_right.
-Save.
+Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).
+auto. Qed.
+
+Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).
+auto. Qed.
+
+Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n.
+auto. Qed.
+
+Lemma STh_mult_one_left2 : forall n:A, n == 1 * n.
+auto. Qed.
+
+Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.
+auto. Qed.
+
+Lemma STh_opp_def2 : forall n:A, 0 == n + - n.
+auto. Qed.
+
+Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).
+intros.
+rewrite (plus_assoc n m p).
+rewrite (plus_comm n m).
+rewrite <- (plus_assoc m n p).
+trivial.
+Qed.
+
+Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).
+intros.
+rewrite (mult_assoc n m p).
+rewrite (mult_comm n m).
+rewrite <- (mult_assoc m n p).
+trivial.
+Qed.
+
+Hint Resolve STh_plus_permute STh_mult_permute.
+
+Lemma Saux1 : forall a:A, a + a == a -> a == 0.
+intros.
+rewrite <- (plus_zero_left a).
+rewrite (plus_comm 0 a).
+setoid_replace (a + 0) with (a + (a + - a)); auto.
+rewrite (plus_assoc a a (- a)).
+rewrite H.
+apply opp_def.
+Qed.
+
+Lemma STh_mult_zero_left : forall n:A, 0 * n == 0.
+intros.
+apply Saux1.
+rewrite <- (distr_left 0 0 n).
+rewrite (plus_zero_left 0).
+trivial.
+Qed.
+Hint Resolve STh_mult_zero_left.
+
+Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n.
+auto.
+Qed.
+
+Lemma Saux2 : forall x y z:A, x + y == 0 -> x + z == 0 -> y == z.
+intros.
+rewrite <- (plus_zero_left y).
+rewrite <- H0.
+rewrite <- (plus_assoc x z y).
+rewrite (plus_comm z y).
+rewrite (plus_assoc x y z).
+rewrite H.
+auto.
+Qed.
+
+Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y.
+intros.
+apply Saux2 with (x * y); auto.
+rewrite <- (distr_left x (- x) y).
+rewrite (opp_def x).
+auto.
+Qed.
+Hint Resolve STh_opp_mult_left.
+
+Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y).
+auto.
+Qed.
+
+Lemma STh_mult_zero_right : forall n:A, n * 0 == 0.
+intro; rewrite (mult_comm n 0); auto.
+Qed.
+
+Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0.
+intro; rewrite (mult_comm n 0); auto.
+Qed.
+
+Lemma STh_plus_zero_right : forall n:A, n + 0 == n.
+intro; rewrite (plus_comm n 0); auto.
+Qed.
+
+Lemma STh_plus_zero_right2 : forall n:A, n == n + 0.
+intro; rewrite (plus_comm n 0); auto.
+Qed.
+
+Lemma STh_mult_one_right : forall n:A, n * 1 == n.
+intro; rewrite (mult_comm n 1); auto.
+Qed.
+
+Lemma STh_mult_one_right2 : forall n:A, n == n * 1.
+intro; rewrite (mult_comm n 1); auto.
+Qed.
+
+Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y.
+intros.
+rewrite (mult_comm x y).
+rewrite (mult_comm x (- y)).
+auto.
+Qed.
+
+Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y).
+intros.
+rewrite (mult_comm x y).
+rewrite (mult_comm x (- y)).
+auto.
+Qed.
+
+Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y).
+intros.
+apply Saux2 with (x + y); auto.
+rewrite (STh_plus_permute (x + y) (- x) (- y)).
+rewrite <- (plus_assoc x y (- y)).
+rewrite (opp_def y); rewrite (STh_plus_zero_right x).
+rewrite (STh_opp_def2 x); trivial.
+Qed.
+
+Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p).
+auto.
+Qed.
+
+Lemma STh_opp_opp : forall n:A, - - n == n.
+intro.
+apply Saux2 with (- n); auto.
+rewrite (plus_comm (- n) n); auto.
+Qed.
+Hint Resolve STh_opp_opp.
+
+Lemma STh_opp_opp2 : forall n:A, n == - - n.
+auto.
+Qed.
+
+Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y.
+intros.
+rewrite (STh_opp_mult_left2 x (- y)).
+rewrite (STh_opp_mult_right2 x y).
+trivial.
+Qed.
+
+Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y.
+intros.
+apply equiv_sym.
+apply STh_mult_opp_opp.
+Qed.
+
+Lemma STh_opp_zero : - 0 == 0.
+rewrite <- (plus_zero_left (- 0)).
+trivial.
+Qed.
+
+Lemma STh_plus_reg_left : forall n m p:A, n + m == n + p -> m == p.
+intros.
+rewrite <- (plus_zero_left m).
+rewrite <- (plus_zero_left p).
+rewrite <- (opp_def n).
+rewrite (plus_comm n (- n)).
+rewrite <- (plus_assoc (- n) n m).
+rewrite <- (plus_assoc (- n) n p).
+auto.
+Qed.
+
+Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.
+intros.
+apply STh_plus_reg_left with n.
+rewrite (plus_comm n m); rewrite (plus_comm n p); assumption.
+Qed.
+
+Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.
+intros.
+rewrite (mult_comm n (m + p)).
+rewrite (mult_comm n m).
+rewrite (mult_comm n p).
+trivial.
+Qed.
+
+Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).
+intros.
+apply equiv_sym.
+apply STh_distr_right.
+Qed.
 
 End Theory_of_setoid_rings.
 
-Hints Resolve STh_mult_zero_left STh_plus_reg_left : core.
+Hint Resolve STh_mult_zero_left STh_plus_reg_left: core.
 
 Unset Implicit Arguments.
 
 Definition Semi_Setoid_Ring_Theory_of :
   Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
-Intros until 1; Case H.
-Split; Intros; Simpl; EAuto.
+intros until 1; case H.
+split; intros; simpl in |- *; eauto.
 Defined.
 
-Coercion Semi_Setoid_Ring_Theory_of :
-  Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory.
+Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >->
+ Semi_Setoid_Ring_Theory.
 
 
 
@@ -426,4 +424,4 @@ Section power_ring.
 
 End power_ring.
 
-End Setoid_rings.
+End Setoid_rings.
\ No newline at end of file