Ajout des fichiers pour le Ring pour setoides

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

3 files changed, 1623 insertions, 0 deletions

diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
new file mode 100644
index 0000000000..59ccc43d32
--- /dev/null
+++ b/contrib/ring/Setoid_ring.v
@@ -0,0 +1,27 @@
+Require Export Setoid_ring_theory.
+Require Export Quote.
+Require Export Setoid_ring_normalize.
+
+Declare ML Module "ring".
+
+Grammar tactic simple_tactic : ast :=
+  ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
+
+Syntax tactic level 0:
+  ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] 
+| ring_e [ << (Ring) >> ] -> ["Ring"].
+
+Grammar vernac vernac : ast := 
+| addsetoidring [ "Add" "Setoid" "Ring"
+      	    constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) 
+	    constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
+	    constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
+  -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
+      	 ($LIST $l))]
+| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" 
+      	  constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
+	  constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) 
+          constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
+  -> [(AddSemiSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
+      	   ($LIST $l))]
+.
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
new file mode 100644
index 0000000000..bba383b01c
--- /dev/null
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -0,0 +1,1142 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Setoid_ring_theory.
+Require Quote.
+
+Implicit Arguments On.
+
+Lemma index_eq_prop: (n,m:index)(Is_true (index_eq n m)) -> n=m.
+Proof.
+  Induction n; Induction m; Simpl; Try (Reflexivity Orelse Contradiction).
+  Intros; Rewrite (H i0); Trivial.
+  Intros; Rewrite (H i0); Trivial.
+Save.
+
+Section setoid.
+
+Variable A : Type.
+Variable Aequiv : A -> A -> Prop.
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aopp : A -> A.
+Variable Aeq : A -> A -> bool.
+
+Variable S : (Setoid_Theory A Aequiv).
+
+Add Setoid A Aequiv S.
+
+Variable plus_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)).
+Variable mult_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)).
+Variable opp_morph : (a,a0:A)
+ (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)).
+
+Add Morphism Aplus : Aplus_ext.
+Exact plus_morph.
+Save.
+
+Add Morphism Amult : Amult_ext.
+Exact mult_morph.
+Save.
+
+Add Morphism Aopp : Aopp_ext.
+Exact opp_morph.
+Save.
+
+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 equiv_refl equiv_trans.
+Hints Immediate equiv_sym.
+
+Section semi_setoid_rings.
+
+(* Section definitions. *)
+
+
+(******************************************)
+(* Normal abtract Polynomials             *)
+(******************************************)
+(* DEFINITIONS :
+- A varlist is a sorted product of one or more variables : x, x*y*z 
+- A monom is a constant, a varlist or the product of a constant by a varlist
+  variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
+- A canonical sum is either a monom or an ordered sum of monoms 
+  (the order on monoms is defined later) 
+- A normal polynomial it either a constant or a canonical sum or a constant
+  plus a canonical sum
+*)
+
+(* varlist is isomorphic to (list var), but we built a special inductive
+   for efficiency *)
+Inductive varlist : Type := 
+| Nil_var : varlist
+| Cons_var : index -> varlist -> varlist
+.
+
+Inductive canonical_sum : Type := 
+| Nil_monom : canonical_sum
+| Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
+| Cons_varlist : varlist -> canonical_sum -> canonical_sum 
+.
+
+(* Order on monoms *)
+
+(* That's the lexicographic order on varlist, extended by : 
+  - A constant is less than every monom 
+  - The relation between two varlist is preserved by multiplication by a
+  constant.
+
+  Examples : 
+  3 < x < y
+  x*y < x*y*y*z 
+  2*x*y < x*y*y*z
+  x*y < 54*x*y*y*z
+  4*x*y < 59*x*y*y*z
+*)
+
+Fixpoint varlist_eq [x,y:varlist] : bool :=
+  Cases x y of
+  | Nil_var Nil_var => true
+  | (Cons_var i xrest) (Cons_var j yrest) => 
+        (andb (index_eq i j) (varlist_eq xrest yrest))
+  | _ _ => false
+  end.
+
+Fixpoint varlist_lt [x,y:varlist] : bool :=
+  Cases x y of 
+  | Nil_var (Cons_var _ _) => true
+  | (Cons_var i xrest) (Cons_var j yrest) => 
+      	if (index_lt i j) then true
+        else (andb (index_eq i j) (varlist_lt xrest yrest))
+  | _ _ => false
+  end.
+
+(* merges two variables lists *)
+Fixpoint varlist_merge [l1:varlist] : varlist -> varlist :=
+  Cases l1 of	
+  | (Cons_var v1 t1) => 
+      Fix vm_aux {vm_aux [l2:varlist] : varlist :=
+	Cases l2 of
+	| (Cons_var v2 t2) => 
+		     if (index_lt v1 v2)
+		     then (Cons_var v1 (varlist_merge t1 l2))
+		     else (Cons_var v2 (vm_aux t2))
+	| Nil_var => l1
+	end}
+  | Nil_var => [l2]l2
+  end.
+
+(* returns the sum of two canonical sums  *)
+Fixpoint canonical_sum_merge [s1:canonical_sum] 
+      	 : canonical_sum -> canonical_sum :=
+Cases s1 of
+| (Cons_monom c1 l1 t1) =>      
+     Fix csm_aux{csm_aux[s2:canonical_sum] : canonical_sum :=
+           Cases s2 of
+      	   | (Cons_monom c2 l2 t2) =>
+      	       if (varlist_eq l1 l2)
+	       then (Cons_monom (Aplus c1 c2) l1 
+      	       	       	        (canonical_sum_merge t1 t2))
+	       else if (varlist_lt l1 l2)
+	       then (Cons_monom c1 l1 (canonical_sum_merge t1 s2))
+	       else (Cons_monom c2 l2 (csm_aux t2))
+      	   | (Cons_varlist l2 t2) =>
+      	       if (varlist_eq l1 l2)
+	       then (Cons_monom (Aplus c1 Aone) l1 
+      	       	       	        (canonical_sum_merge t1 t2))
+	       else if (varlist_lt l1 l2)
+	       then (Cons_monom c1 l1 (canonical_sum_merge t1 s2))
+	       else (Cons_varlist l2 (csm_aux t2))
+	   | Nil_monom => s1
+	   end}
+| (Cons_varlist l1 t1) =>      
+     Fix csm_aux2{csm_aux2[s2:canonical_sum] : canonical_sum :=
+           Cases s2 of
+      	   | (Cons_monom c2 l2 t2) =>
+      	       if (varlist_eq l1 l2)
+	       then (Cons_monom (Aplus Aone c2) l1 
+      	       	       	        (canonical_sum_merge t1 t2))
+	       else if (varlist_lt l1 l2)
+	       then (Cons_varlist l1 (canonical_sum_merge t1 s2))
+	       else (Cons_monom c2 l2 (csm_aux2 t2))
+      	   | (Cons_varlist l2 t2) =>
+      	       if (varlist_eq l1 l2)
+	       then (Cons_monom (Aplus Aone Aone) l1 
+      	       	       	        (canonical_sum_merge t1 t2))
+	       else if (varlist_lt l1 l2)
+	       then (Cons_varlist l1 (canonical_sum_merge t1 s2))
+	       else (Cons_varlist l2 (csm_aux2 t2))
+	   | Nil_monom => s1
+	   end}
+| Nil_monom => [s2]s2
+end.
+
+(* Insertion of a monom in a canonical sum *)
+Fixpoint monom_insert [c1:A; l1:varlist; s2 : canonical_sum] 
+      : canonical_sum := 
+  Cases s2 of
+  | (Cons_monom c2 l2 t2) =>
+       if (varlist_eq l1 l2)
+       then (Cons_monom (Aplus c1 c2) l1 t2)
+       else if (varlist_lt l1 l2)
+       then (Cons_monom c1 l1 s2)
+       else (Cons_monom c2 l2 (monom_insert c1 l1 t2))
+  | (Cons_varlist l2 t2) =>
+       if (varlist_eq l1 l2)
+       then (Cons_monom (Aplus c1 Aone) l1 t2)
+       else if (varlist_lt l1 l2)
+       then (Cons_monom c1 l1 s2)
+       else (Cons_varlist l2 (monom_insert c1 l1 t2))
+  | Nil_monom => (Cons_monom c1 l1 Nil_monom)
+  end.
+
+Fixpoint varlist_insert [l1:varlist; s2:canonical_sum] 
+      : canonical_sum :=
+  Cases s2 of
+  | (Cons_monom c2 l2 t2) =>
+       if (varlist_eq l1 l2)
+       then (Cons_monom (Aplus Aone c2) l1 t2)
+       else if (varlist_lt l1 l2)
+       then (Cons_varlist l1 s2)
+       else (Cons_monom c2 l2 (varlist_insert l1 t2))
+  | (Cons_varlist l2 t2) =>
+       if (varlist_eq l1 l2)
+       then (Cons_monom (Aplus Aone Aone) l1 t2)
+       else if (varlist_lt l1 l2)
+       then (Cons_varlist l1 s2)
+       else (Cons_varlist l2 (varlist_insert l1 t2))
+  | Nil_monom => (Cons_varlist l1 Nil_monom)
+  end.
+
+(* Computes c0*s *)
+Fixpoint canonical_sum_scalar [c0:A; s:canonical_sum] : canonical_sum :=
+    Cases s of
+    | (Cons_monom c l t) => 
+	(Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t))
+    | (Cons_varlist l t) => 
+	(Cons_monom c0 l (canonical_sum_scalar c0 t))
+    | Nil_monom => Nil_monom
+    end.
+
+(* Computes l0*s  *)
+Fixpoint canonical_sum_scalar2 [l0:varlist; s:canonical_sum] 
+      	       	       	      : canonical_sum :=
+    Cases s of
+    | (Cons_monom c l t) => 
+      	  (monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t))
+    | (Cons_varlist l t) => 
+          (varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t))
+    | Nil_monom  => Nil_monom
+    end.
+
+(* Computes c0*l0*s  *)
+Fixpoint canonical_sum_scalar3 [c0:A;l0:varlist; s:canonical_sum] 
+      	       	       	      : canonical_sum :=
+    Cases s of
+    | (Cons_monom c l t) => 
+          (monom_insert (Amult c0 c) (varlist_merge l0 l) 
+                        (canonical_sum_scalar3 c0 l0 t))
+    | (Cons_varlist l t) => 
+      	  (monom_insert c0 (varlist_merge l0 l) 
+                          (canonical_sum_scalar3 c0 l0 t))
+    | Nil_monom  => Nil_monom
+    end.
+
+(* returns the product of two canonical sums *) 
+Fixpoint canonical_sum_prod [s1:canonical_sum] 
+      	 : canonical_sum -> canonical_sum := 
+    [s2]Cases s1 of
+    | (Cons_monom c1 l1 t1) =>
+	(canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2) 
+			     (canonical_sum_prod t1 s2))
+    | (Cons_varlist l1 t1) =>
+	(canonical_sum_merge (canonical_sum_scalar2 l1 s2) 
+			     (canonical_sum_prod t1 s2))
+    | Nil_monom => Nil_monom
+    end.
+
+(* The type to represent concrete semi-setoid-ring polynomials *)
+
+Inductive Type setspolynomial :=
+  SetSPvar : index -> setspolynomial
+| SetSPconst : A -> setspolynomial
+| SetSPplus : setspolynomial -> setspolynomial -> setspolynomial
+| SetSPmult : setspolynomial -> setspolynomial -> setspolynomial.
+
+Fixpoint setspolynomial_normalize [p:setspolynomial] : canonical_sum :=
+ Cases p of
+ | (SetSPplus l r) => (canonical_sum_merge (setspolynomial_normalize l) (setspolynomial_normalize r))
+ | (SetSPmult l r) => (canonical_sum_prod (setspolynomial_normalize l) (setspolynomial_normalize r))
+ | (SetSPconst c)  => (Cons_monom c Nil_var Nil_monom)
+ | (SetSPvar i)    => (Cons_varlist (Cons_var i Nil_var) Nil_monom)
+ end.
+
+Fixpoint canonical_sum_simplify [ s:canonical_sum] : canonical_sum :=
+  Cases s of
+  | (Cons_monom c l t) => 
+	 if (Aeq c Azero) 
+	 then (canonical_sum_simplify t)
+	 else if (Aeq c Aone)
+	 then (Cons_varlist l (canonical_sum_simplify t))
+	 else (Cons_monom c l (canonical_sum_simplify t))
+  | (Cons_varlist l t) => (Cons_varlist l (canonical_sum_simplify t))
+  | Nil_monom => Nil_monom
+  end.
+
+Definition setspolynomial_simplify :=
+  [x:setspolynomial] (canonical_sum_simplify (setspolynomial_normalize x)).
+
+Variable vm : (varmap A).
+
+Definition interp_var [i:index] := (varmap_find Azero i vm).
+
+Definition ivl_aux := Fix ivl_aux {ivl_aux[x:index; t:varlist] : A := 
+  Cases t of
+  | Nil_var => (interp_var x)
+  | (Cons_var x' t') => (Amult (interp_var x) (ivl_aux x' t'))
+  end}.
+
+Definition interp_vl :=  [l:varlist] 
+  Cases l of
+  | Nil_var => Aone
+  | (Cons_var x t) => (ivl_aux x t)
+  end.
+
+Definition interp_m := [c:A][l:varlist] 
+  Cases l of
+  | Nil_var => c
+  | (Cons_var x t) => 
+      (Amult c (ivl_aux x t))
+  end.
+
+Definition ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A :=  
+  Cases s of
+  | Nil_monom => a
+  | (Cons_varlist l t) => (Aplus a (ics_aux (interp_vl l) t))
+  | (Cons_monom c l t) => (Aplus a (ics_aux (interp_m c l) t))
+  end}.
+
+Definition interp_cs : canonical_sum -> A  := 
+  [s]Cases s of 
+  | Nil_monom => Azero
+  | (Cons_varlist l t) =>
+      	(ics_aux (interp_vl l) t)
+  | (Cons_monom c l t) =>
+      	(ics_aux (interp_m c l) t)
+  end.
+
+Fixpoint interp_setsp [p:setspolynomial] : A :=
+ Cases p of
+ | (SetSPconst c) => c
+ | (SetSPvar i) => (interp_var i)
+ | (SetSPplus p1 p2) => (Aplus (interp_setsp p1) (interp_setsp p2))
+ | (SetSPmult p1 p2) => (Amult (interp_setsp p1) (interp_setsp p2))
+ end.
+
+(* End interpretation. *)
+
+Implicit Arguments Off.
+
+(* Section properties. *)
+
+(**************
+Syntax constr 
+  level 0:
+  fix_cache [<<Fix $x{$_[$_:$_]:$_:=$_}>>] -> [ "Fix " $x ]
+| fix_cache2 [<<Fix $x{$_[$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ]
+| fix_cache3 [<<Fix $x{$_[$_:$_;$_:$_;$_:$_]:$_:=$_}>>] -> [ "Fix " $x ]
+.
+************)
+
+Variable T : (Semi_Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aeq).
+
+Hint SSR_plus_sym_T := Resolve (SSR_plus_sym T).
+Hint SSR_plus_assoc_T := Resolve (SSR_plus_assoc T).
+Hint SSR_plus_assoc2_T := Resolve (SSR_plus_assoc2 S T).
+Hint SSR_mult_sym_T := Resolve (SSR_mult_sym T).
+Hint SSR_mult_assoc_T := Resolve (SSR_mult_assoc T).
+Hint SSR_mult_assoc2_T := Resolve (SSR_mult_assoc2 S T).
+Hint SSR_plus_zero_left_T := Resolve (SSR_plus_zero_left T).
+Hint SSR_plus_zero_left2_T := Resolve (SSR_plus_zero_left2 S T).
+Hint SSR_mult_one_left_T := Resolve (SSR_mult_one_left T).
+Hint SSR_mult_one_left2_T := Resolve (SSR_mult_one_left2 S T).
+Hint SSR_mult_zero_left_T := Resolve (SSR_mult_zero_left T).
+Hint SSR_mult_zero_left2_T := Resolve (SSR_mult_zero_left2 S T).
+Hint SSR_distr_left_T := Resolve (SSR_distr_left T).
+Hint SSR_distr_left2_T := Resolve (SSR_distr_left2 S T).
+Hint SSR_plus_reg_left_T := Resolve (SSR_plus_reg_left T).
+Hint SSR_plus_permute_T := Resolve (SSR_plus_permute S plus_morph T).
+Hint SSR_mult_permute_T := Resolve (SSR_mult_permute S mult_morph T).
+Hint SSR_distr_right_T := Resolve (SSR_distr_right S plus_morph T).
+Hint SSR_distr_right2_T := Resolve (SSR_distr_right2 S plus_morph T).
+Hint SSR_mult_zero_right_T := Resolve (SSR_mult_zero_right S T).
+Hint SSR_mult_zero_right2_T := Resolve (SSR_mult_zero_right2 S T).
+Hint SSR_plus_zero_right_T := Resolve (SSR_plus_zero_right S T).
+Hint SSR_plus_zero_right2_T := Resolve (SSR_plus_zero_right2 S T).
+Hint SSR_mult_one_right_T := Resolve (SSR_mult_one_right S T).
+Hint SSR_mult_one_right2_T := Resolve (SSR_mult_one_right2 S T).
+Hint SSR_plus_reg_right_T := Resolve (SSR_plus_reg_right S T).
+Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Immediate T.
+
+Lemma varlist_eq_prop : (x,y:varlist)
+  (Is_true (varlist_eq x y))->x==y.
+Proof.
+  Induction x; Induction y; Contradiction Orelse Try Reflexivity.
+  Simpl; Intros.
+  Generalize (andb_prop2 ? ? H1); Intros; Elim H2; Intros.
+  Rewrite (index_eq_prop H3); Rewrite (H v0 H4); Reflexivity.
+Save.
+
+Remark ivl_aux_ok : (v:varlist)(i:index)
+  (Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v))).
+Proof.
+  Induction v; Simpl; Intros.
+  Trivial.
+  Setoid_rewrite (H i); Trivial.
+Save.
+
+Lemma varlist_merge_ok : (x,y:varlist)
+  (Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y))).
+Proof.
+  Induction x.
+  Simpl; Trivial.
+  Induction y.
+  Simpl; Trivial.
+  Simpl; Intros.
+  Elim (index_lt i i0); Simpl; Intros.
+
+  Setoid_rewrite (ivl_aux_ok v i).
+  Setoid_rewrite (ivl_aux_ok v0 i0).
+  Setoid_rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i).
+  Setoid_rewrite (H (Cons_var i0 v0)).
+  Simpl.
+  Setoid_rewrite (ivl_aux_ok v0 i0).
+  EAuto.
+
+  Setoid_rewrite (ivl_aux_ok v i).
+  Setoid_rewrite (ivl_aux_ok v0 i0).
+  Setoid_rewrite (ivl_aux_ok
+                 (Fix vm_aux
+                    {vm_aux [l2:varlist] : varlist :=
+                       Cases (l2) of
+                         Nil_var => (Cons_var i v)
+                       | (Cons_var v2 t2) => 
+                          (if (index_lt i v2)
+                           then (Cons_var i (varlist_merge v l2))
+                           else (Cons_var v2 (vm_aux t2)))
+                       end} v0) i0).
+  Setoid_rewrite H0.
+  Setoid_rewrite (ivl_aux_ok v i).
+  EAuto.
+Save.
+
+Remark ics_aux_ok : (x:A)(s:canonical_sum)
+  (Aequiv (ics_aux x s) (Aplus x (interp_cs s))).
+Proof.
+ Induction s; Simpl; Intros;Trivial.
+Save.
+
+Remark interp_m_ok : (x:A)(l:varlist)
+  (Aequiv (interp_m x l) (Amult x (interp_vl l))).
+Proof.
+  Destruct l;Trivial.
+Save.
+
+Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_merge x y))
+  (Aplus (interp_cs x) (interp_cs y))).
+Proof.
+Induction x; Simpl.
+Trivial.
+
+Induction y; Simpl; Intros.
+EAuto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c).
+Setoid_rewrite (ics_aux_ok (interp_m a0 v0) c0).
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus a a0) v0)
+                 (canonical_sum_merge c c0)).
+Setoid_rewrite (H c0).
+Setoid_rewrite (interp_m_ok (Aplus a a0) v0).
+Setoid_rewrite (interp_m_ok a v0).
+Setoid_rewrite (interp_m_ok a0 v0).
+Setoid_replace (Amult (Aplus a a0) (interp_vl v0))
+ with (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0))).
+Setoid_replace (Aplus
+                 (Aplus (Amult a (interp_vl v0))
+                   (Amult a0 (interp_vl v0)))
+                 (Aplus (interp_cs c) (interp_cs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+        (Aplus (Amult a0 (interp_vl v0))
+          (Aplus (interp_cs c) (interp_cs c0)))).
+Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_cs c))
+                 (Aplus (Amult a0 (interp_vl v0)) (interp_cs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+        (Aplus (interp_cs c)
+          (Aplus (Amult a0 (interp_vl v0)) (interp_cs c0)))).
+Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Intro.
+Setoid_rewrite (ics_aux_ok (interp_m a v)
+                 (canonical_sum_merge c (Cons_monom a0 v0 c0))).
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (ics_aux_ok (interp_m a0 v0) c0).
+Setoid_rewrite (H (Cons_monom a0 v0 c0)); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m a0 v0) c0); Auto.
+
+Intro.
+Setoid_rewrite (ics_aux_ok (interp_m a0 v0)
+                 (Fix csm_aux
+                    {csm_aux [s2:canonical_sum] : canonical_sum :=
+                       Cases (s2) of
+                         Nil_monom => (Cons_monom a v c)
+                       | (Cons_monom c2 l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus a c2) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_monom a v
+                                (canonical_sum_merge c s2))
+                             else (Cons_monom c2 l2 (csm_aux t2))))
+                       | (Cons_varlist l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus a Aone) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_monom a v
+                                (canonical_sum_merge c s2))
+                             else (Cons_varlist l2 (csm_aux t2))))
+                       end} c0)).
+Setoid_rewrite H0.
+Setoid_rewrite (ics_aux_ok (interp_m a v) c);
+Setoid_rewrite (ics_aux_ok (interp_m a0 v0) c0); Simpl; Auto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0)
+                 (canonical_sum_merge c c0));
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0).
+Setoid_rewrite (H c0).
+Setoid_rewrite (interp_m_ok (Aplus a Aone) v0).
+Setoid_rewrite (interp_m_ok a v0).
+Setoid_replace (Amult (Aplus a Aone) (interp_vl v0))
+ with (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0))).
+Setoid_replace (Aplus
+                 (Aplus (Amult a (interp_vl v0))
+                   (Amult Aone (interp_vl v0)))
+                 (Aplus (interp_cs c) (interp_cs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+        (Aplus (Amult Aone (interp_vl v0))
+          (Aplus (interp_cs c) (interp_cs c0)))).
+Setoid_replace (Aplus (Aplus (Amult a (interp_vl v0)) (interp_cs c))
+                 (Aplus (interp_vl v0) (interp_cs c0)))
+ with (Aplus (Amult a (interp_vl v0))
+        (Aplus (interp_cs c) (Aplus (interp_vl v0) (interp_cs c0)))).
+Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0).
+Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Intro.
+Setoid_rewrite (ics_aux_ok (interp_m a v)
+                 (canonical_sum_merge c (Cons_varlist v0 c0)));
+Setoid_rewrite (ics_aux_ok (interp_m a v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0).
+Setoid_rewrite (H (Cons_varlist v0 c0)); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0).
+Auto.
+
+Intro.
+Setoid_rewrite (ics_aux_ok (interp_vl v0)
+                 (Fix csm_aux
+                    {csm_aux [s2:canonical_sum] : canonical_sum :=
+                       Cases (s2) of
+                         Nil_monom => (Cons_monom a v c)
+                       | (Cons_monom c2 l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus a c2) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_monom a v
+                                (canonical_sum_merge c s2))
+                             else (Cons_monom c2 l2 (csm_aux t2))))
+                       | (Cons_varlist l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus a Aone) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_monom a v
+                                (canonical_sum_merge c s2))
+                             else (Cons_varlist l2 (csm_aux t2))))
+                       end} c0)); Setoid_rewrite H0.
+Setoid_rewrite (ics_aux_ok (interp_m a v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0); Simpl.
+Auto.
+
+Induction y; Simpl; Intros.
+Trivial.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0).
+Intros; Rewrite (H1 I).
+Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0)
+                 (canonical_sum_merge c c0));
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c);
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c0); Setoid_rewrite (
+H c0).
+Setoid_rewrite (interp_m_ok (Aplus Aone a) v0);
+Setoid_rewrite (interp_m_ok a v0).
+Setoid_replace (Amult (Aplus Aone a) (interp_vl v0))
+ with (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
+Setoid_replace (Aplus
+                 (Aplus (Amult Aone (interp_vl v0))
+                   (Amult a (interp_vl v0)))
+                 (Aplus (interp_cs c) (interp_cs c0)))
+ with (Aplus (Amult Aone (interp_vl v0))
+        (Aplus (Amult a (interp_vl v0))
+          (Aplus (interp_cs c) (interp_cs c0))));
+Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_cs c))
+                 (Aplus (Amult a (interp_vl v0)) (interp_cs c0)))
+ with (Aplus (interp_vl v0)
+        (Aplus (interp_cs c)
+          (Aplus (Amult a (interp_vl v0)) (interp_cs c0)))).
+Auto.
+
+Elim (varlist_lt v v0); Simpl; Intros.
+Setoid_rewrite (ics_aux_ok (interp_vl v)
+                 (canonical_sum_merge c (Cons_monom a v0 c0)));
+Setoid_rewrite (ics_aux_ok (interp_vl v) c);
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c0).
+Setoid_rewrite (H (Cons_monom a v0 c0)); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c0); Auto.
+
+Setoid_rewrite (ics_aux_ok (interp_m a v0)
+                 (Fix csm_aux2
+                    {csm_aux2 [s2:canonical_sum] : canonical_sum :=
+                       Cases (s2) of
+                         Nil_monom => (Cons_varlist v c)
+                       | (Cons_monom c2 l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus Aone c2) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_varlist v
+                                (canonical_sum_merge c s2))
+                             else (Cons_monom c2 l2 (csm_aux2 t2))))
+                       | (Cons_varlist l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus Aone Aone) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_varlist v
+                                (canonical_sum_merge c s2))
+                             else (Cons_varlist l2 (csm_aux2 t2))))
+                       end} c0)); Setoid_rewrite H0.
+Setoid_rewrite (ics_aux_ok (interp_vl v) c);
+Setoid_rewrite (ics_aux_ok (interp_m a v0) c0); Simpl; Auto.
+
+Generalize (varlist_eq_prop v v0).
+Elim (varlist_eq v v0); Intros.
+Rewrite (H1 I); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v0)
+                 (canonical_sum_merge c c0));
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0); Setoid_rewrite (
+H c0).
+Setoid_rewrite (interp_m_ok (Aplus Aone Aone) v0).
+Setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0))
+ with (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
+Setoid_replace (Aplus
+                 (Aplus (Amult Aone (interp_vl v0))
+                   (Amult Aone (interp_vl v0)))
+                 (Aplus (interp_cs c) (interp_cs c0)))
+ with (Aplus (Amult Aone (interp_vl v0))
+        (Aplus (Amult Aone (interp_vl v0))
+          (Aplus (interp_cs c) (interp_cs c0))));
+Setoid_replace (Aplus (Aplus (interp_vl v0) (interp_cs c))
+                 (Aplus (interp_vl v0) (interp_cs c0)))
+ with (Aplus (interp_vl v0)
+        (Aplus (interp_cs c) (Aplus (interp_vl v0) (interp_cs c0)))).
+Setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); Auto.
+
+Elim (varlist_lt v v0); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_vl v)
+                 (canonical_sum_merge c (Cons_varlist v0 c0)));
+Setoid_rewrite (ics_aux_ok (interp_vl v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0);
+Setoid_rewrite (H (Cons_varlist v0 c0)); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0); Auto.
+
+Setoid_rewrite (ics_aux_ok (interp_vl v0)
+                 (Fix csm_aux2
+                    {csm_aux2 [s2:canonical_sum] : canonical_sum :=
+                       Cases (s2) of
+                         Nil_monom => (Cons_varlist v c)
+                       | (Cons_monom c2 l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus Aone c2) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_varlist v
+                                (canonical_sum_merge c s2))
+                             else (Cons_monom c2 l2 (csm_aux2 t2))))
+                       | (Cons_varlist l2 t2) => 
+                          (if (varlist_eq v l2)
+                           then
+                            (Cons_monom (Aplus Aone Aone) v
+                              (canonical_sum_merge c t2))
+                           else
+                            (if (varlist_lt v l2)
+                             then
+                              (Cons_varlist v
+                                (canonical_sum_merge c s2))
+                             else (Cons_varlist l2 (csm_aux2 t2))))
+                       end} c0)); Setoid_rewrite H0.
+Setoid_rewrite (ics_aux_ok (interp_vl v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v0) c0); Simpl; Auto.
+Save.
+
+Lemma monom_insert_ok: (a:A)(l:varlist)(s:canonical_sum)
+ (Aequiv (interp_cs (monom_insert a l s)) 
+   (Aplus (Amult a (interp_vl l)) (interp_cs s))).
+Proof.
+Induction s; Intros.
+Simpl; Setoid_rewrite (interp_m_ok a l); Trivial.
+
+Simpl; Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c);
+Setoid_rewrite (ics_aux_ok (interp_m a0 v) c).
+Setoid_rewrite (interp_m_ok (Aplus a a0) v);
+Setoid_rewrite (interp_m_ok a0 v).
+Setoid_replace (Amult (Aplus a a0) (interp_vl v))
+ with (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v))).
+Auto.
+
+Elim (varlist_lt l v); Simpl; Intros.
+Setoid_rewrite (ics_aux_ok (interp_m a0 v) c).
+Setoid_rewrite (interp_m_ok a0 v); Setoid_rewrite (interp_m_ok a l).
+Auto.
+
+Setoid_rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c));
+Setoid_rewrite (ics_aux_ok (interp_m a0 v) c); Setoid_rewrite H.
+Auto.
+
+Simpl.
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v) c).
+Setoid_rewrite (interp_m_ok (Aplus a Aone) v).
+Setoid_replace (Amult (Aplus a Aone) (interp_vl v))
+ with (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v).
+Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Setoid_rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c));
+Setoid_rewrite H.
+Setoid_rewrite (ics_aux_ok (interp_vl v) c); Auto.
+Save.
+
+Lemma varlist_insert_ok :
+ (l:varlist)(s:canonical_sum)
+ (Aequiv (interp_cs (varlist_insert l s)) 
+   (Aplus (interp_vl l) (interp_cs s))).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c);
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok (Aplus Aone a) v);
+Setoid_rewrite (interp_m_ok a v).
+Setoid_replace (Amult (Aplus Aone a) (interp_vl v))
+ with (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Setoid_rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c));
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite H; Auto.
+
+Generalize (varlist_eq_prop l v); Elim (varlist_eq l v).
+Intro Hr; Rewrite (Hr I); Simpl.
+Setoid_rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c);
+Setoid_rewrite (ics_aux_ok (interp_vl v) c).
+Setoid_rewrite (interp_m_ok (Aplus Aone Aone) v).
+Setoid_replace (Amult (Aplus Aone Aone) (interp_vl v))
+ with (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v))).
+Setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); Auto.
+
+Elim (varlist_lt l v); Simpl; Intros; Auto.
+Setoid_rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)).
+Setoid_rewrite H.
+Setoid_rewrite (ics_aux_ok (interp_vl v) c); Auto.
+Save.
+
+Lemma canonical_sum_scalar_ok : (a:A)(s:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_scalar a s)) (Amult a (interp_cs s))).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Setoid_rewrite (ics_aux_ok (interp_m (Amult a a0) v)
+                 (canonical_sum_scalar a c));
+Setoid_rewrite (ics_aux_ok (interp_m a0 v) c).
+Setoid_rewrite (interp_m_ok (Amult a a0) v);
+Setoid_rewrite (interp_m_ok a0 v).
+Setoid_rewrite H.
+Setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_cs c)))
+ with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_cs c))).
+Auto.
+
+Setoid_rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
+Setoid_rewrite (ics_aux_ok (interp_vl v) c); Setoid_rewrite H.
+Setoid_rewrite (interp_m_ok a v).
+Auto.
+Save.
+
+Lemma canonical_sum_scalar2_ok : (l:varlist; s:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_scalar2 l s)) (Amult (interp_vl l) (interp_cs s))).
+Proof.
+Induction s; Simpl; Intros; Auto.
+Setoid_rewrite (monom_insert_ok a (varlist_merge l v)
+                 (canonical_sum_scalar2 l c)).
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite H.
+Setoid_rewrite (varlist_merge_ok l v).
+Setoid_replace (Amult (interp_vl l)
+                 (Aplus (Amult a (interp_vl v)) (interp_cs c)))
+ with (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+        (Amult (interp_vl l) (interp_cs c))).
+Auto.
+
+Setoid_rewrite (varlist_insert_ok (varlist_merge l v)
+                 (canonical_sum_scalar2 l c)).
+Setoid_rewrite (ics_aux_ok (interp_vl v) c).
+Setoid_rewrite H.
+Setoid_rewrite (varlist_merge_ok l v).
+Auto.
+Save.
+
+Lemma canonical_sum_scalar3_ok : (c:A; l:varlist; s:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_scalar3 c l s)) (Amult c (Amult (interp_vl l) (interp_cs s)))).
+Proof.
+Induction s; Simpl; Intros.
+Setoid_rewrite (SSR_mult_zero_right S T (interp_vl l)).
+Auto.
+
+Setoid_rewrite (monom_insert_ok (Amult c a) (varlist_merge l v)
+                 (canonical_sum_scalar3 c l c0)).
+Setoid_rewrite (ics_aux_ok (interp_m a v) c0).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite H.
+Setoid_rewrite (varlist_merge_ok l v).
+Setoid_replace (Amult (interp_vl l)
+                 (Aplus (Amult a (interp_vl v)) (interp_cs c0)))
+ with (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+        (Amult (interp_vl l) (interp_cs c0))).
+Setoid_replace (Amult c
+                 (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
+                   (Amult (interp_vl l) (interp_cs c0))))
+ with (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
+        (Amult c (Amult (interp_vl l) (interp_cs c0)))).
+Setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v)))
+ with (Amult c (Amult a (Amult (interp_vl l) (interp_vl v)))).
+Auto.
+
+Setoid_rewrite (monom_insert_ok c (varlist_merge l v)
+                 (canonical_sum_scalar3 c l c0)).
+Setoid_rewrite (ics_aux_ok (interp_vl v) c0).
+Setoid_rewrite H.
+Setoid_rewrite (varlist_merge_ok l v).
+Setoid_replace (Aplus (Amult c (Amult (interp_vl l) (interp_vl v)))
+                 (Amult c (Amult (interp_vl l) (interp_cs c0))))
+ with (Amult c
+        (Aplus (Amult (interp_vl l) (interp_vl v))
+          (Amult (interp_vl l) (interp_cs c0)))).
+Auto.
+Save.
+
+Lemma canonical_sum_prod_ok : (x,y:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_prod x y)) (Amult (interp_cs x) (interp_cs y))).
+Proof.
+Induction x; Simpl; Intros.
+Trivial.
+
+Setoid_rewrite (canonical_sum_merge_ok (canonical_sum_scalar3 a v y)
+                 (canonical_sum_prod c y)).
+Setoid_rewrite (canonical_sum_scalar3_ok a v y).
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite (H y).
+Setoid_replace (Amult a (Amult (interp_vl v) (interp_cs y)))
+ with (Amult (Amult a (interp_vl v)) (interp_cs y)).
+Setoid_replace (Amult (Aplus (Amult a (interp_vl v)) (interp_cs c))
+                 (interp_cs y))
+ with (Aplus (Amult (Amult a (interp_vl v)) (interp_cs y))
+        (Amult (interp_cs c) (interp_cs y))).
+Trivial.
+
+Setoid_rewrite (canonical_sum_merge_ok (canonical_sum_scalar2 v y)
+                 (canonical_sum_prod c y)).
+Setoid_rewrite (canonical_sum_scalar2_ok v y).
+Setoid_rewrite (ics_aux_ok (interp_vl v) c).
+Setoid_rewrite (H y).
+Trivial.
+Save.
+
+Theorem setspolynomial_normalize_ok : (p:setspolynomial)
+  (Aequiv (interp_cs (setspolynomial_normalize p)) (interp_setsp p)).
+Proof.
+Induction p; Simpl; Intros; Trivial.
+Setoid_rewrite (canonical_sum_merge_ok (setspolynomial_normalize s)
+                 (setspolynomial_normalize s0)).
+Setoid_rewrite H; Setoid_rewrite H0; Trivial.
+
+Setoid_rewrite (canonical_sum_prod_ok (setspolynomial_normalize s)
+                 (setspolynomial_normalize s0)).
+Setoid_rewrite H; Setoid_rewrite H0; Trivial.
+Save.
+
+Lemma canonical_sum_simplify_ok : (s:canonical_sum)
+  (Aequiv (interp_cs (canonical_sum_simplify s)) (interp_cs s)).
+Proof.
+Induction s; Simpl; Intros.
+Trivial.
+
+Generalize (SSR_eq_prop T 9!a 10!Azero).
+Elim (Aeq a Azero).
+Simpl.
+Intros.
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite (H0 I).
+Setoid_replace (Amult Azero (interp_vl v)) with Azero.
+Setoid_rewrite H.
+Trivial.
+
+Intros; Simpl.
+Generalize (SSR_eq_prop T 9!a 10!Aone).
+Elim (Aeq a Aone).
+Intros.
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite (interp_m_ok a v).
+Setoid_rewrite (H1 I).
+Simpl.
+Setoid_rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
+Setoid_rewrite H.
+Auto.
+
+Simpl.
+Intros.
+Setoid_rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)).
+Setoid_rewrite (ics_aux_ok (interp_m a v) c).
+Setoid_rewrite H; Trivial.
+
+Setoid_rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
+Setoid_rewrite H.
+Auto.
+Save.
+
+Theorem setspolynomial_simplify_ok : (p:setspolynomial)
+  (Aequiv (interp_cs (setspolynomial_simplify p)) (interp_setsp p)).
+Proof.
+Intro.
+Unfold setspolynomial_simplify.
+Setoid_rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)).
+Exact (setspolynomial_normalize_ok p).
+Save.
+
+End semi_setoid_rings.
+
+Implicits Cons_varlist.
+Implicits Cons_monom.
+Implicits SetSPconst.
+Implicits SetSPplus.
+Implicits SetSPmult.
+
+
+
+Section setoid_rings.
+
+Implicit Arguments On.
+
+Variable vm : (varmap A).
+Variable T : (Setoid_Ring_Theory A Aequiv Aplus Amult Aone Azero Aopp Aeq).
+
+Hint STh_plus_sym_T := Resolve (STh_plus_sym T).
+Hint STh_plus_assoc_T := Resolve (STh_plus_assoc T).
+Hint STh_plus_assoc2_T := Resolve (STh_plus_assoc2 S T).
+Hint STh_mult_sym_T := Resolve (STh_mult_sym T).
+Hint STh_mult_assoc_T := Resolve (STh_mult_assoc T).
+Hint STh_mult_assoc2_T := Resolve (STh_mult_assoc2 S T).
+Hint STh_plus_zero_left_T := Resolve (STh_plus_zero_left T).
+Hint STh_plus_zero_left2_T := Resolve (STh_plus_zero_left2 S T).
+Hint STh_mult_one_left_T := Resolve (STh_mult_one_left T).
+Hint STh_mult_one_left2_T := Resolve (STh_mult_one_left2 S T).
+Hint STh_mult_zero_left_T := Resolve (STh_mult_zero_left S plus_morph mult_morph T).
+Hint STh_mult_zero_left2_T := Resolve (STh_mult_zero_left2 S plus_morph mult_morph T).
+Hint STh_distr_left_T := Resolve (STh_distr_left T).
+Hint STh_distr_left2_T := Resolve (STh_distr_left2 S T).
+Hint STh_plus_reg_left_T := Resolve (STh_plus_reg_left S plus_morph T).
+Hint STh_plus_permute_T := Resolve (STh_plus_permute S plus_morph T).
+Hint STh_mult_permute_T := Resolve (STh_mult_permute S mult_morph T).
+Hint STh_distr_right_T := Resolve (STh_distr_right S plus_morph T).
+Hint STh_distr_right2_T := Resolve (STh_distr_right2 S plus_morph T).
+Hint STh_mult_zero_right_T := Resolve (STh_mult_zero_right S plus_morph mult_morph T).
+Hint STh_mult_zero_right2_T := Resolve (STh_mult_zero_right2 S plus_morph mult_morph T).
+Hint STh_plus_zero_right_T := Resolve (STh_plus_zero_right S T).
+Hint STh_plus_zero_right2_T := Resolve (STh_plus_zero_right2 S T).
+Hint STh_mult_one_right_T := Resolve (STh_mult_one_right S T).
+Hint STh_mult_one_right2_T := Resolve (STh_mult_one_right2 S T).
+Hint STh_plus_reg_right_T := Resolve (STh_plus_reg_right S plus_morph T).
+Hints Resolve refl_eqT sym_eqT trans_eqT.
+Hints Immediate T.
+
+
+(*** Definitions *)
+
+Inductive Type setpolynomial := 
+  SetPvar : index -> setpolynomial
+| SetPconst : A -> setpolynomial
+| SetPplus : setpolynomial -> setpolynomial -> setpolynomial
+| SetPmult : setpolynomial -> setpolynomial -> setpolynomial
+| SetPopp : setpolynomial -> setpolynomial.
+
+Fixpoint setpolynomial_normalize [x:setpolynomial] : canonical_sum :=
+ Cases x of
+ | (SetPplus l r) => (canonical_sum_merge
+     (setpolynomial_normalize l) 
+     (setpolynomial_normalize r))
+ | (SetPmult l r) => (canonical_sum_prod
+     (setpolynomial_normalize l)
+     (setpolynomial_normalize r))
+ | (SetPconst c)  => (Cons_monom c Nil_var Nil_monom)
+ | (SetPvar i)    => (Cons_varlist (Cons_var i Nil_var) Nil_monom)
+ | (SetPopp p)    => (canonical_sum_scalar3
+     (Aopp Aone) Nil_var
+     (setpolynomial_normalize p))
+ end.
+
+Definition setpolynomial_simplify :=
+ [x:setpolynomial](canonical_sum_simplify (setpolynomial_normalize x)).
+
+Fixpoint setspolynomial_of [x:setpolynomial] : setspolynomial :=
+ Cases x of 
+ | (SetPplus l r) => (SetSPplus (setspolynomial_of l) (setspolynomial_of r))
+ | (SetPmult l r) => (SetSPmult (setspolynomial_of l) (setspolynomial_of r))
+ | (SetPconst c)  => (SetSPconst c)
+ | (SetPvar i)    => (SetSPvar i)
+ | (SetPopp p)    => (SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p))
+ end.
+
+(*** Interpretation *)
+
+Fixpoint interp_setp [p:setpolynomial] : A :=
+ Cases p of
+ | (SetPconst c)    => c
+ | (SetPvar i)      => (varmap_find Azero i vm)
+ | (SetPplus p1 p2) => (Aplus (interp_setp p1) (interp_setp p2))
+ | (SetPmult p1 p2) => (Amult (interp_setp p1) (interp_setp p2))
+ | (SetPopp p1)     => (Aopp (interp_setp p1))
+ end.
+
+(*** Properties *)
+
+Implicit Arguments Off.
+
+Lemma setspolynomial_of_ok : (p:setpolynomial)
+ (Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p))).
+Induction p; Trivial; Simpl; Intros.
+Setoid_rewrite H; Setoid_rewrite H0; Trivial.
+Setoid_rewrite H; Setoid_rewrite H0; Trivial.
+Setoid_rewrite H.
+Setoid_rewrite (STh_opp_mult_left2 S plus_morph mult_morph T Aone
+                 (interp_setsp vm (setspolynomial_of s))).
+Setoid_rewrite (STh_mult_one_left T
+                 (interp_setsp vm (setspolynomial_of s))).
+Trivial.
+Save.
+
+Theorem setpolynomial_normalize_ok : (p:setpolynomial)
+ (setpolynomial_normalize p)
+  ==(setspolynomial_normalize (setspolynomial_of p)).
+Induction p; Trivial; Simpl; Intros.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Rewrite H0; Reflexivity.
+Rewrite H; Simpl.
+Elim (canonical_sum_scalar3 (Aopp Aone) Nil_var
+   (setspolynomial_normalize (setspolynomial_of s)));
+ [ Reflexivity
+ | Simpl; Intros; Rewrite H0; Reflexivity
+ | Simpl; Intros; Rewrite H0; Reflexivity ].
+Save.
+
+Theorem setpolynomial_simplify_ok : (p:setpolynomial)
+ (Aequiv (interp_cs vm (setpolynomial_simplify p)) (interp_setp p)).
+Intro.
+Unfold setpolynomial_simplify.
+Setoid_rewrite (setspolynomial_of_ok p).
+Rewrite setpolynomial_normalize_ok.
+Setoid_rewrite (canonical_sum_simplify_ok vm
+   (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp
+    Aeq plus_morph mult_morph T)
+   (setspolynomial_normalize (setspolynomial_of p))).
+Setoid_rewrite (setspolynomial_normalize_ok vm 
+   (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp
+    Aeq plus_morph mult_morph T) (setspolynomial_of p)).
+Trivial.
+Save.
+
+End setoid_rings.
+
+End setoid.
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
new file mode 100644
index 0000000000..6428947ec0
--- /dev/null
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -0,0 +1,454 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+Require Export Bool.
+Require Export Setoid_replace.
+
+Implicit Arguments On.
+
+Grammar ring formula : constr :=
+  formula_expr [ expr($p) ] -> [$p]
+| formula_eq [ expr($p) "==" expr($c) ] -> [ (Aequiv $p $c) ]
+
+with expr : constr :=
+  RIGHTA
+    expr_plus [ expr($p) "+" expr($c) ] -> [ (Aplus $p $c) ]
+  | expr_expr1 [ expr1($p) ] -> [$p]
+
+with expr1 : constr :=
+  RIGHTA
+    expr1_plus [ expr1($p) "*" expr1($c) ] -> [ (Amult $p $c) ]
+  | expr1_final [ final($p) ] -> [$p]
+
+with final : constr :=
+  final_var [ prim:var($id) ] -> [ $id ]
+| final_constr [ "[" constr:constr($c) "]" ] -> [ $c ]
+| final_app [ "(" application($r) ")" ] -> [ $r ]
+| final_0 [ "0" ] -> [ Azero ]
+| final_1 [ "1" ] -> [ Aone ]
+| final_uminus [ "-" expr($c) ] -> [ (Aopp $c) ]
+
+with application : constr :=
+  LEFTA
+    app_cons [ application($p) application($c1) ] -> [ ($p $c1) ]
+  | app_tail [ expr($c1) ] -> [ $c1 ].
+
+Grammar constr constr0 :=
+  formula_in_constr [ "[" "|" ring:formula($c) "|" "]" ] -> [ $c ].
+
+Section Setoid_rings.
+
+Variable A : Type.
+Variable Aequiv : A -> A -> Prop.
+
+Variable S : (Setoid_Theory A Aequiv).
+
+Add Setoid A Aequiv S.
+
+Variable Aplus : A -> A -> A.
+Variable Amult : A -> A -> A.
+Variable Aone : A.
+Variable Azero : A.
+Variable Aopp : A -> A.
+Variable Aeq : A -> A -> bool.
+
+Variable plus_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Aplus a a1) (Aplus a0 a2)).
+Variable mult_morph : (a,a0,a1,a2:A)
+ (Aequiv a a0)->(Aequiv a1 a2)->(Aequiv (Amult a a1) (Amult a0 a2)).
+Variable opp_morph : (a,a0:A)
+ (Aequiv a a0)->(Aequiv (Aopp a) (Aopp a0)).
+
+Add Morphism Aplus : Aplus_ext.
+Exact plus_morph.
+Save.
+
+Add Morphism Amult : Amult_ext.
+Exact mult_morph.
+Save.
+
+Add Morphism Aopp : Aopp_ext.
+Exact opp_morph.
+Save.
+
+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 |] -> (Aequiv m p);
+  SSR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> (Aequiv 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.
+
+(* 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.
+
+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)) -> (Aequiv 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.
+
+(* 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|] -> (Aequiv 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)(Aequiv (Aplus (Amult n m) (Amult n p)) (Amult n (Aplus m p))).
+Intros.
+Apply equiv_sym.
+Apply STh_distr_right.
+Save.
+
+End Theory_of_setoid_rings.
+
+Hints Resolve STh_mult_zero_left STh_plus_reg_left : core.
+
+Implicit Arguments Off.
+
+Definition Semi_Setoid_Ring_Theory_of :
+  Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
+Destruct 1.
+Split; Intros; Simpl; EAuto.
+Defined.
+
+Coercion Semi_Setoid_Ring_Theory_of :
+  Setoid_Ring_Theory >-> Semi_Setoid_Ring_Theory.
+
+
+
+Section product_ring.
+
+End product_ring.
+
+Section power_ring.
+
+End power_ring.
+
+End Setoid_rings.