additional properties for FMap (and slight rework of SetoidList and FSetProperties)

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

6 files changed, 126 insertions, 157 deletions

diff --git a/.depend b/.depend
index f74a5bd683..f1d77c104c 100644
--- a/.depend
+++ b/.depend
@@ -3984,18 +3984,18 @@ contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
 contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
     pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
-    proofs/redexpr.cmi pretyping/rawterm.cmi parsing/printer.cmi lib/pp.cmi \
-    kernel/names.cmi library/libnames.cmi pretyping/inductiveops.cmi \
-    kernel/inductive.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
-    kernel/environ.cmi kernel/conv_oracle.cmi contrib/xml/acic.cmo \
+    pretyping/rawterm.cmi parsing/printer.cmi lib/pp.cmi kernel/names.cmi \
+    library/libnames.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
+    kernel/closure.cmi contrib/xml/acic.cmo \
     contrib/xml/doubleTypeInference.cmi 
 contrib/xml/doubleTypeInference.cmx: lib/util.cmx contrib/xml/unshare.cmx \
     kernel/typeops.cmx pretyping/termops.cmx kernel/term.cmx \
     pretyping/retyping.cmx pretyping/reductionops.cmx kernel/reduction.cmx \
-    proofs/redexpr.cmx pretyping/rawterm.cmx parsing/printer.cmx lib/pp.cmx \
-    kernel/names.cmx library/libnames.cmx pretyping/inductiveops.cmx \
-    kernel/inductive.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
-    kernel/environ.cmx kernel/conv_oracle.cmx contrib/xml/acic.cmx \
+    pretyping/rawterm.cmx parsing/printer.cmx lib/pp.cmx kernel/names.cmx \
+    library/libnames.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \
+    kernel/closure.cmx contrib/xml/acic.cmx \
     contrib/xml/doubleTypeInference.cmi 
 contrib/xml/proof2aproof.cmo: lib/util.cmi contrib/xml/unshare.cmi \
     pretyping/termops.cmi kernel/term.cmi parsing/tactic_printer.cmi \
@@ -4024,25 +4024,25 @@ contrib/xml/unshare.cmx: contrib/xml/unshare.cmi
 contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \
     lib/util.cmi contrib/xml/unshare.cmi kernel/typeops.cmi kernel/term.cmi \
     proofs/tacmach.cmi pretyping/recordops.cmi proofs/proof_trees.cmi \
-    contrib/xml/proof2aproof.cmo proofs/pfedit.cmi library/nametab.cmi \
-    kernel/names.cmi library/library.cmi library/libobject.cmi \
-    library/libnames.cmi library/lib.cmi parsing/lexer.cmi \
-    pretyping/inductiveops.cmi kernel/inductive.cmi library/global.cmi \
-    pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \
-    library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
-    config/coq_config.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
-    contrib/xml/acic.cmo contrib/xml/xmlcommand.cmi 
+    contrib/xml/proof2aproof.cmo lib/pp.cmi proofs/pfedit.cmi \
+    library/nametab.cmi kernel/names.cmi library/library.cmi \
+    library/libobject.cmi library/libnames.cmi library/lib.cmi \
+    parsing/lexer.cmi pretyping/inductiveops.cmi kernel/inductive.cmi \
+    library/global.cmi pretyping/evd.cmi pretyping/evarutil.cmi \
+    kernel/environ.cmi library/declare.cmi kernel/declarations.cmi \
+    library/decl_kinds.cmo config/coq_config.cmi contrib/xml/cic2acic.cmo \
+    contrib/xml/acic2Xml.cmo contrib/xml/acic.cmo contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlcommand.cmx: contrib/xml/xml.cmx toplevel/vernac.cmx \
     lib/util.cmx contrib/xml/unshare.cmx kernel/typeops.cmx kernel/term.cmx \
     proofs/tacmach.cmx pretyping/recordops.cmx proofs/proof_trees.cmx \
-    contrib/xml/proof2aproof.cmx proofs/pfedit.cmx library/nametab.cmx \
-    kernel/names.cmx library/library.cmx library/libobject.cmx \
-    library/libnames.cmx library/lib.cmx parsing/lexer.cmx \
-    pretyping/inductiveops.cmx kernel/inductive.cmx library/global.cmx \
-    pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \
-    library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \
-    config/coq_config.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
-    contrib/xml/acic.cmx contrib/xml/xmlcommand.cmi 
+    contrib/xml/proof2aproof.cmx lib/pp.cmx proofs/pfedit.cmx \
+    library/nametab.cmx kernel/names.cmx library/library.cmx \
+    library/libobject.cmx library/libnames.cmx library/lib.cmx \
+    parsing/lexer.cmx pretyping/inductiveops.cmx kernel/inductive.cmx \
+    library/global.cmx pretyping/evd.cmx pretyping/evarutil.cmx \
+    kernel/environ.cmx library/declare.cmx kernel/declarations.cmx \
+    library/decl_kinds.cmx config/coq_config.cmx contrib/xml/cic2acic.cmx \
+    contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx contrib/xml/xmlcommand.cmi 
 contrib/xml/xmlentries.cmo: contrib/xml/xmlcommand.cmi \
     toplevel/vernacinterp.cmi lib/util.cmi lib/pp.cmi parsing/pcoq.cmi \
     parsing/lexer.cmi interp/genarg.cmi parsing/extend.cmi \
diff --git a/.depend.coq b/.depend.coq
index 72416e2c72..df645a7792 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -282,54 +282,6 @@ theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contri
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
 theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
 theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.vo
-theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo
-theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo
-theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo
-theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo
-theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo contrib/setoid_ring/ArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo
-theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo
-theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo
-theories/Reals/Rcomplete.vo: theories/Reals/Rcomplete.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo
-theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplete.vo theories/Arith/Max.vo
-theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/Binomial.vo: theories/Reals/Binomial.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo
-theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binomial.vo
-theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo
-theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo
-theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo
-theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo
-theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo
-theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo
-theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo
-theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo
-theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo
-theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo
-theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo
-theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo
-theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo
-theories/Reals/MVT.vo: theories/Reals/MVT.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo
-theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo
-theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo
-theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo
-theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo
-theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo
-theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo
-theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo
-theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo
-theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/MVT.vo theories/Reals/Ranalysis4.vo
-theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/MVT.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo
-theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo
-theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo
-theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo
-theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo
-theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo
 theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 115f75dc4d..9a23a398e0 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -568,6 +568,7 @@ Module Properties (M: S).
 
   Definition cardinal (m:t elt) := length (elements m).
 
+  Definition Equal (m m':t elt) := forall y, find y m = find y m'.
   Definition Add x (e:elt) m m' := forall y, find y m' = find y (add x e m).
 
   Definition Above x (m:t elt) := forall y, In y m -> E.lt y x.
@@ -768,6 +769,16 @@ Module Properties (M: S).
   ME.order.
   Qed.
 
+  Lemma elements_Equal_eqlistA : forall (m m': t elt), 
+   Equal m m' -> eqlistA eqke (elements m) (elements m').
+  Proof.
+  intros.
+  apply sort_equivlistA_eqlistA; auto.
+  red; intros.
+  destruct x; do 2 rewrite <- elements_mapsto_iff.
+  do 2 rewrite find_mapsto_iff; rewrite H; split; auto.
+  Qed.
+
   End Elements.
 
   Section Cardinal.
@@ -1022,6 +1033,48 @@ Module Properties (M: S).
   Qed.
 
   End Induction_Principles.
+
+  Section Fold_properties.
+
+  Lemma fold_Equal : forall s1 s2 (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op (@O.eqke _) eqA (fun y =>f (fst y) (snd y)) -> 
+   Equal s1 s2 -> 
+   eqA (fold f s1 i) (fold f s2 i).
+  Proof.
+  intros.
+  do 2 rewrite fold_1.
+  do 2 rewrite <- fold_left_rev_right.
+  apply fold_right_eqlistA with (eqA:=@O.eqke _) (eqB:=eqA); auto.
+  apply eqlistA_rev.
+  apply elements_Equal_eqlistA; auto.
+  Qed.
+
+  Lemma fold_Add : forall s1 s2 x e (A:Set)(eqA:A->A->Prop)(st:Setoid_Theory A eqA)
+   (f:key->elt->A->A)(i:A), 
+   compat_op (@O.eqke _) eqA (fun y =>f (fst y) (snd y)) -> 
+   transpose eqA (fun y =>f (fst y) (snd y)) -> 
+   ~In x s1 -> Add x e s1 s2 -> 
+   eqA (fold f s2 i) (f x e (fold f s1 i)).
+  Proof.
+  intros; do 2 rewrite fold_1; do 2 rewrite <- fold_left_rev_right.
+  set (f':=fun (y:key*elt) x0 => f (fst y) (snd y) x0) in *.
+  change (f x e (fold_right f' i (rev (elements s1))))
+   with (f' (x,e) (fold_right f' i (rev (elements s1)))).
+  trans_st (fold_right f' i (rev ((filter (gtb (x, e)) (elements s1) ++
+                              (x, e) :: filter (leb (x, e)) (elements s1))))).
+  apply fold_right_eqlistA with (eqA:=@eqke _) (eqB:=eqA); auto.
+  apply eqlistA_rev.
+  apply elements_Add; auto.
+  rewrite distr_rev; simpl.
+  rewrite app_ass; simpl.
+  pattern (elements s1) at 3; rewrite (elements_split (x,e) s1).
+  rewrite distr_rev; simpl.
+  apply fold_right_commutes with (eqA:=@eqke _) (eqB:=eqA); auto.
+  Qed.
+
+  End Fold_properties.
+
  End Elt.
 
 End Properties.
diff --git a/theories/FSets/FMapWeakFacts.v b/theories/FSets/FMapWeakFacts.v
index af8dccf536..ccd29be882 100644
--- a/theories/FSets/FMapWeakFacts.v
+++ b/theories/FSets/FMapWeakFacts.v
@@ -508,51 +508,6 @@ rewrite (find_1 H4) in H0; discriminate.
 rewrite (find_1 H4) in H1; discriminate.
 Qed.
 
-Fixpoint findA (A B:Set)(f : A -> bool) (l:list (A*B)) : option B := 
- match l with  
-  | nil => None 
-  | (a,b)::l => if f a then Some b else findA f l
- end.
-
-Lemma findA_NoDupA : 
- forall (A B:Set)
- (eqA:A->A->Prop)
- (eqA_sym: forall a b, eqA a b -> eqA b a)
- (eqA_trans: forall a b c, eqA a b -> eqA b c -> eqA a c)
- (eqA_dec : forall a a', { eqA a a' }+{~eqA a a' }) 
- (l:list (A*B))(x:A)(e:B),  
- NoDupA (fun p p' => eqA (fst p) (fst p')) l -> 
- (InA (fun p p' => eqA (fst p) (fst p') /\ snd p = snd p') (x,e) l <->
-  findA (fun y:A => if eqA_dec x y then true else false) l = Some e).
-Proof.
-induction l; simpl; intros.
-split; intros; try discriminate.
-inversion H0.
-destruct a as (y,e').
-inversion_clear H.
-split; intros.
-inversion_clear H.
-simpl in *; destruct H2; subst e'.
-destruct (eqA_dec x y); intuition.
-destruct (eqA_dec x y); simpl.
-destruct H0.
-generalize e0 H2 eqA_trans eqA_sym; clear.
-induction l.
-inversion 2.
-inversion_clear 2; intros; auto.
-destruct a.
-compute in H; destruct H.
-subst b.
-constructor 1; auto.
-simpl.
-apply eqA_trans with x; auto.
-rewrite <- IHl; auto.
-destruct (eqA_dec x y); simpl in *.
-inversion H; clear H; intros; subst e'; auto.
-constructor 2.
-rewrite IHl; auto.
-Qed.
-
 Lemma elements_o : forall m x, 
  find x m = findA (eqb x) (elements m).
 Proof.
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 21ca1120c6..4039e5bbbc 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -783,14 +783,17 @@ Module Properties (M: S).
    transpose eqA f ->
    ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
   Proof.
-  intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); 
-    destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))).
-  rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2.
-  apply fold_right_add with (eqA:=E.eq)(eqB:=eqA); auto.
-  eauto.
-  exact eq_dec.
-  rewrite <- Hl1; auto.
-  intros; rewrite <- Hl1; rewrite <- Hl'1; auto.
+  intros; do 2 rewrite M.fold_1; do 2 rewrite <- fold_left_rev_right.
+  trans_st (fold_right f i (rev ((List.filter (gtb x) (elements s) ++
+                                 x :: List.filter (leb x) (elements s))))).
+  apply fold_right_eqlistA with (eqA:=E.eq) (eqB:=eqA); auto.
+  apply eqlistA_rev.
+  apply elements_Add; auto.
+  rewrite distr_rev; simpl.
+  rewrite app_ass; simpl.
+  pattern (elements s) at 3; rewrite (elements_split x s).
+  rewrite distr_rev; simpl.
+  apply fold_right_commutes with (eqA:=E.eq) (eqB:=eqA); auto.
   Qed.
 
   (** More properties of [fold] : behavior with respect to Above/Below *) 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 74b2812231..ab470f2ae3 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -387,8 +387,43 @@ case_eq (f a); auto; intros.
 rewrite H3 in H; auto; try discriminate.
 Qed.
 
+Section Fold.
+
+Variable B:Set.
+Variable eqB:B->B->Prop.
+
+(** Compatibility of a two-argument function with respect to two equalities. *)
+Definition compat_op (f : A -> B -> B) :=
+  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
+
+(** Two-argument functions that allow to reorder their arguments. *)
+Definition transpose (f : A -> B -> B) :=
+  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
+
+Variable st:Setoid_Theory _ eqB.
+Variable f:A->B->B.
+Variable i:B.
+Variable Comp:compat_op f.
+
+Lemma fold_right_eqlistA : 
+   forall s s', eqlistA s s' -> 
+   eqB (fold_right f i s) (fold_right f i s').
+Proof.
+induction 1; simpl; auto.
+refl_st.
+Qed.
+
+Variable Ass:transpose f.
+
+Lemma fold_right_commutes : forall s1 s2 x, 
+  eqB (fold_right f i (s1++x::s2)) (f x (fold_right f i (s1++s2))).
+Proof.
+induction s1; simpl; auto; intros.
+refl_st.
+trans_st (f a (f x (fold_right f i (s1++s2)))).
+Qed.
 
-Section Remove.
+Section Remove_And_More_Fold.
 
 Hypothesis eqA_dec : forall x y : A, {eqA x y}+{~(eqA x y)}.
 
@@ -492,26 +527,6 @@ inversion_clear H7; auto.
 elim H6; auto.
 Qed.
 
-
-Section Fold.
-
-Variable B:Set.
-Variable eqB:B->B->Prop.
-
-(** Compatibility of a two-argument function with respect to two equalities. *)
-Definition compat_op (f : A -> B -> B) :=
-  forall (x x' : A) (y y' : B), eqA x x' -> eqB y y' -> eqB (f x y) (f x' y').
-
-(** Two-argument functions that allow to reorder their arguments. *)
-Definition transpose (f : A -> B -> B) :=
-  forall (x y : A) (z : B), eqB (f x (f y z)) (f y (f x z)). 
-
-Variable st:Setoid_Theory _ eqB.
-Variable f:A->B->B.
-Variable Comp:compat_op f.
-Variable Ass:transpose f.
-Variable i:B.
-
 Lemma removeA_fold_right_0 :
   forall s x, ~InA x s ->
   eqB (fold_right f i s) (fold_right f i (removeA x s)).
@@ -564,15 +579,6 @@ Proof.
  rewrite <- E; auto.
 Qed.
 
-(* for this one, the transpose hyp is not required *)
-Lemma fold_right_eqlistA : 
-   forall s s', eqlistA s s' -> 
-   eqB (fold_right f i s) (fold_right f i s').
-Proof.
-induction 1; simpl; auto.
-refl_st.
-Qed.
-
 Lemma fold_right_add :
   forall s' s x, NoDupA s -> NoDupA s' -> ~ InA x s ->
   addlistA x s s' -> eqB (fold_right f i s') (f x (fold_right f i s)).
@@ -613,9 +619,9 @@ Proof.
  destruct H; auto; destruct n; auto.
 Qed.
 
-End Fold.
+End Remove_And_More_Fold.
 
-End Remove.
+End Fold.
 
 End Type_with_equality.