1 files changed, 164 insertions, 163 deletions

diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v
index 80ab2b2c..ec0c6a55 100644
--- a/theories/FSets/FSetEqProperties.v
+++ b/theories/FSets/FSetEqProperties.v
@@ -6,15 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-(* $Id: FSetEqProperties.v 11720 2008-12-28 07:12:15Z letouzey $ *)
+(* $Id$ *)
 
 (** * Finite sets library *)
 
-(** This module proves many properties of finite sets that 
-    are consequences of the axiomatization in [FsetInterface] 
-    Contrary to the functor in [FsetProperties] it uses 
+(** This module proves many properties of finite sets that
+    are consequences of the axiomatization in [FsetInterface]
+    Contrary to the functor in [FsetProperties] it uses
     sets operations instead of predicates over sets, i.e.
-    [mem x s=true] instead of [In x s], 
+    [mem x s=true] instead of [In x s],
     [equal s s'=true] instead of [Equal s s'], etc. *)
 
 Require Import FSetProperties Zerob Sumbool Omega DecidableTypeEx.
@@ -26,59 +26,59 @@ Import M.
 
 Definition Add := MP.Add.
 
-Section BasicProperties. 
+Section BasicProperties.
 
-(** Some old specifications written with boolean equalities. *) 
+(** Some old specifications written with boolean equalities. *)
 
 Variable s s' s'': t.
 Variable x y z : elt.
 
-Lemma mem_eq: 
+Lemma mem_eq:
   E.eq x y -> mem x s=mem y s.
-Proof. 
+Proof.
 intro H; rewrite H; auto.
 Qed.
 
-Lemma equal_mem_1: 
+Lemma equal_mem_1:
   (forall a, mem a s=mem a s') -> equal s s'=true.
-Proof. 
+Proof.
 intros; apply equal_1; unfold Equal; intros.
 do 2 rewrite mem_iff; rewrite H; tauto.
 Qed.
 
-Lemma equal_mem_2: 
+Lemma equal_mem_2:
   equal s s'=true -> forall a, mem a s=mem a s'.
-Proof. 
+Proof.
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma subset_mem_1: 
+Lemma subset_mem_1:
   (forall a, mem a s=true->mem a s'=true) -> subset s s'=true.
-Proof. 
+Proof.
 intros; apply subset_1; unfold Subset; intros a.
 do 2 rewrite mem_iff; auto.
 Qed.
 
-Lemma subset_mem_2: 
+Lemma subset_mem_2:
   subset s s'=true -> forall a, mem a s=true -> mem a s'=true.
-Proof. 
+Proof.
 intros H a; do 2 rewrite <- mem_iff; apply subset_2; auto.
 Qed.
-  
+
 Lemma empty_mem: mem x empty=false.
-Proof. 
+Proof.
 rewrite <- not_mem_iff; auto with set.
 Qed.
 
 Lemma is_empty_equal_empty: is_empty s = equal s empty.
-Proof. 
+Proof.
 apply bool_1; split; intros.
 auto with set.
 rewrite <- is_empty_iff; auto with set.
 Qed.
-  
+
 Lemma choose_mem_1: choose s=Some x -> mem x s=true.
-Proof.  
+Proof.
 auto with set.
 Qed.
 
@@ -90,44 +90,44 @@ Qed.
 Lemma add_mem_1: mem x (add x s)=true.
 Proof.
 auto with set.
-Qed.  
- 
+Qed.
+
 Lemma add_mem_2: ~E.eq x y -> mem y (add x s)=mem y s.
-Proof. 
+Proof.
 apply add_neq_b.
 Qed.
 
 Lemma remove_mem_1: mem x (remove x s)=false.
-Proof. 
+Proof.
 rewrite <- not_mem_iff; auto with set.
-Qed. 
- 
+Qed.
+
 Lemma remove_mem_2: ~E.eq x y -> mem y (remove x s)=mem y s.
-Proof. 
+Proof.
 apply remove_neq_b.
 Qed.
 
-Lemma singleton_equal_add: 
+Lemma singleton_equal_add:
   equal (singleton x) (add x empty)=true.
 Proof.
 rewrite (singleton_equal_add x); auto with set.
-Qed.  
+Qed.
 
-Lemma union_mem: 
+Lemma union_mem:
   mem x (union s s')=mem x s || mem x s'.
-Proof. 
+Proof.
 apply union_b.
 Qed.
 
-Lemma inter_mem: 
+Lemma inter_mem:
   mem x (inter s s')=mem x s && mem x s'.
-Proof. 
+Proof.
 apply inter_b.
 Qed.
 
-Lemma diff_mem: 
+Lemma diff_mem:
   mem x (diff s s')=mem x s && negb (mem x s').
-Proof. 
+Proof.
 apply diff_b.
 Qed.
 
@@ -143,7 +143,7 @@ Proof.
 intros; rewrite not_mem_iff; auto.
 Qed.
 
-(** Properties of [equal] *) 
+(** Properties of [equal] *)
 
 Lemma equal_refl: equal s s=true.
 Proof.
@@ -155,19 +155,19 @@ Proof.
 intros; apply bool_1; do 2 rewrite <- equal_iff; intuition.
 Qed.
 
-Lemma equal_trans: 
+Lemma equal_trans:
  equal s s'=true -> equal s' s''=true -> equal s s''=true.
 Proof.
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma equal_equal: 
+Lemma equal_equal:
  equal s s'=true -> equal s s''=equal s' s''.
 Proof.
 intros; rewrite (equal_2 H); auto.
 Qed.
 
-Lemma equal_cardinal: 
+Lemma equal_cardinal:
  equal s s'=true -> cardinal s=cardinal s'.
 Proof.
 auto with set.
@@ -175,25 +175,25 @@ Qed.
 
 (* Properties of [subset] *)
 
-Lemma subset_refl: subset s s=true. 
+Lemma subset_refl: subset s s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma subset_antisym: 
+Lemma subset_antisym:
  subset s s'=true -> subset s' s=true -> equal s s'=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma subset_trans: 
+Lemma subset_trans:
  subset s s'=true -> subset s' s''=true -> subset s s''=true.
 Proof.
 do 3 rewrite <- subset_iff; intros.
 apply subset_trans with s'; auto.
 Qed.
 
-Lemma subset_equal: 
+Lemma subset_equal:
  equal s s'=true -> subset s s'=true.
 Proof.
 auto with set.
@@ -201,7 +201,7 @@ Qed.
 
 (** Properties of [choose] *)
 
-Lemma choose_mem_3: 
+Lemma choose_mem_3:
  is_empty s=false -> {x:elt|choose s=Some x /\ mem x s=true}.
 Proof.
 intros.
@@ -221,13 +221,13 @@ Qed.
 
 (** Properties of [add] *)
 
-Lemma add_mem_3: 
+Lemma add_mem_3:
  mem y s=true -> mem y (add x s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma add_equal: 
+Lemma add_equal:
  mem x s=true -> equal (add x s) s=true.
 Proof.
 auto with set.
@@ -235,26 +235,26 @@ Qed.
 
 (** Properties of [remove] *)
 
-Lemma remove_mem_3: 
+Lemma remove_mem_3:
  mem y (remove x s)=true -> mem y s=true.
 Proof.
 rewrite remove_b; intros H;destruct (andb_prop _ _ H); auto.
 Qed.
 
-Lemma remove_equal: 
+Lemma remove_equal:
  mem x s=false -> equal (remove x s) s=true.
 Proof.
 intros; apply equal_1; apply remove_equal.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma add_remove: 
+Lemma add_remove:
  mem x s=true -> equal (add x (remove x s)) s=true.
 Proof.
 intros; apply equal_1; apply add_remove; auto with set.
 Qed.
 
-Lemma remove_add: 
+Lemma remove_add:
  mem x s=false -> equal (remove x (add x s)) s=true.
 Proof.
 intros; apply equal_1; apply remove_add; auto.
@@ -297,37 +297,37 @@ Proof.
 auto with set.
 Qed.
 
-Lemma union_subset_equal: 
+Lemma union_subset_equal:
  subset s s'=true -> equal (union s s') s'=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_equal_1: 
+Lemma union_equal_1:
  equal s s'=true-> equal (union s s'') (union s' s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_equal_2: 
+Lemma union_equal_2:
  equal s' s''=true-> equal (union s s') (union s s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_assoc: 
+Lemma union_assoc:
  equal (union (union s s') s'') (union s (union s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma add_union_singleton: 
+Lemma add_union_singleton:
  equal (add x s) (union (singleton x) s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_add: 
+Lemma union_add:
  equal (union (add x s) s') (add x (union s s'))=true.
 Proof.
 auto with set.
@@ -346,62 +346,62 @@ auto with set.
 Qed.
 
 Lemma union_subset_3:
- subset s s''=true -> subset s' s''=true -> 
+ subset s s''=true -> subset s' s''=true ->
   subset (union s s') s''=true.
 Proof.
 intros; apply subset_1; apply union_subset_3; auto with set.
 Qed.
 
-(** Properties of [inter] *) 
+(** Properties of [inter] *)
 
 Lemma inter_sym: equal (inter s s') (inter s' s)=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_subset_equal: 
+Lemma inter_subset_equal:
  subset s s'=true -> equal (inter s s') s=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_equal_1: 
+Lemma inter_equal_1:
  equal s s'=true -> equal (inter s s'') (inter s' s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_equal_2: 
+Lemma inter_equal_2:
  equal s' s''=true -> equal (inter s s') (inter s s'')=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_assoc: 
+Lemma inter_assoc:
  equal (inter (inter s s') s'') (inter s (inter s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_inter_1: 
+Lemma union_inter_1:
  equal (inter (union s s') s'') (union (inter s s'') (inter s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma union_inter_2: 
+Lemma union_inter_2:
  equal (union (inter s s') s'') (inter (union s s'') (union s' s''))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_add_1: mem x s'=true -> 
+Lemma inter_add_1: mem x s'=true ->
  equal (inter (add x s) s') (add x (inter s s'))=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma inter_add_2: mem x s'=false -> 
+Lemma inter_add_2: mem x s'=false ->
  equal (inter (add x s) s') (inter s s')=true.
 Proof.
 intros; apply equal_1; apply inter_add_2.
@@ -421,7 +421,7 @@ auto with set.
 Qed.
 
 Lemma inter_subset_3:
- subset s'' s=true -> subset s'' s'=true -> 
+ subset s'' s=true -> subset s'' s'=true ->
   subset s'' (inter s s')=true.
 Proof.
 intros; apply subset_1; apply inter_subset_3; auto with set.
@@ -440,19 +440,19 @@ Proof.
 auto with set.
 Qed.
 
-Lemma remove_inter_singleton: 
+Lemma remove_inter_singleton:
  equal (remove x s) (diff s (singleton x))=true.
 Proof.
 auto with set.
 Qed.
 
 Lemma diff_inter_empty:
- equal (inter (diff s s') (inter s s')) empty=true. 
+ equal (inter (diff s s') (inter s s')) empty=true.
 Proof.
 auto with set.
 Qed.
 
-Lemma diff_inter_all: 
+Lemma diff_inter_all:
  equal (union (diff s s') (inter s s')) s=true.
 Proof.
 auto with set.
@@ -462,7 +462,7 @@ End BasicProperties.
 
 Hint Immediate empty_mem is_empty_equal_empty add_mem_1
    remove_mem_1 singleton_equal_add union_mem inter_mem
-   diff_mem equal_sym add_remove remove_add : set. 
+   diff_mem equal_sym add_remove remove_add : set.
 Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
    choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal
    subset_refl subset_equal subset_antisym
@@ -472,8 +472,8 @@ Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1
 (** General recursion principle *)
 
 Lemma set_rec:  forall (P:t->Type),
- (forall s s', equal s s'=true -> P s -> P s') -> 
- (forall s x, mem x s=false -> P s -> P (add x s)) -> 
+ (forall s s', equal s s'=true -> P s -> P s') ->
+ (forall s x, mem x s=false -> P s -> P (add x s)) ->
  P empty -> forall s, P s.
 Proof.
 intros.
@@ -493,51 +493,51 @@ intros; do 2 rewrite mem_iff.
 destruct (mem x s); destruct (mem x s'); intuition.
 Qed.
 
-Section Fold. 
+Section Fold.
 Variables (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA).
 Variables (f:elt->A->A)(Comp:compat_op E.eq eqA f)(Ass:transpose eqA f).
 Variables (i:A).
 Variables (s s':t)(x:elt).
- 
+
 Lemma fold_empty: (fold f empty i) = i.
-Proof. 
+Proof.
 apply fold_empty; auto.
 Qed.
 
-Lemma fold_equal: 
+Lemma fold_equal:
  equal s s'=true -> eqA (fold f s i) (fold f s' i).
-Proof. 
+Proof.
 intros; apply fold_equal with (eqA:=eqA); auto with set.
 Qed.
-   
-Lemma fold_add: 
+
+Lemma fold_add:
  mem x s=false -> eqA (fold f (add x s) i) (f x (fold f s i)).
-Proof. 
+Proof.
 intros; apply fold_add with (eqA:=eqA); auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma add_fold: 
+Lemma add_fold:
   mem x s=true -> eqA (fold f (add x s) i) (fold f s i).
 Proof.
 intros; apply add_fold with (eqA:=eqA); auto with set.
 Qed.
 
-Lemma remove_fold_1: 
+Lemma remove_fold_1:
  mem x s=true -> eqA (f x (fold f (remove x s) i)) (fold f s i).
 Proof.
 intros; apply remove_fold_1 with (eqA:=eqA); auto with set.
 Qed.
 
-Lemma remove_fold_2: 
+Lemma remove_fold_2:
  mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
 Proof.
 intros; apply remove_fold_2 with (eqA:=eqA); auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma fold_union: 
- (forall x, mem x s && mem x s'=false) -> 
+Lemma fold_union:
+ (forall x, mem x s && mem x s'=false) ->
  eqA (fold f (union s s') i) (fold f s (fold f s' i)).
 Proof.
 intros; apply fold_union with (eqA:=eqA); auto.
@@ -548,40 +548,40 @@ End Fold.
 
 (** Properties of [cardinal] *)
 
-Lemma add_cardinal_1: 
+Lemma add_cardinal_1:
  forall s x, mem x s=true -> cardinal (add x s)=cardinal s.
 Proof.
 auto with set.
 Qed.
 
-Lemma add_cardinal_2: 
+Lemma add_cardinal_2:
  forall s x, mem x s=false -> cardinal (add x s)=S (cardinal s).
 Proof.
 intros; apply add_cardinal_2; auto.
 rewrite not_mem_iff; auto.
 Qed.
 
-Lemma remove_cardinal_1: 
+Lemma remove_cardinal_1:
  forall s x, mem x s=true -> S (cardinal (remove x s))=cardinal s.
 Proof.
 intros; apply remove_cardinal_1; auto with set.
 Qed.
 
-Lemma remove_cardinal_2: 
+Lemma remove_cardinal_2:
  forall s x, mem x s=false -> cardinal (remove x s)=cardinal s.
 Proof.
 intros; apply Equal_cardinal; apply equal_2; auto with set.
 Qed.
 
-Lemma union_cardinal: 
- forall s s', (forall x, mem x s && mem x s'=false) -> 
+Lemma union_cardinal:
+ forall s s', (forall x, mem x s && mem x s'=false) ->
  cardinal (union s s')=cardinal s+cardinal s'.
 Proof.
 intros; apply union_cardinal; auto; intros.
 rewrite exclusive_set; auto.
 Qed.
 
-Lemma subset_cardinal: 
+Lemma subset_cardinal:
  forall s s', subset s s'=true -> cardinal s<=cardinal s'.
 Proof.
 intros; apply subset_cardinal; auto with set.
@@ -592,24 +592,24 @@ Section Bool.
 (** Properties of [filter] *)
 
 Variable f:elt->bool.
-Variable Comp: compat_bool E.eq f.
+Variable Comp: Proper (E.eq==>Logic.eq) f.
 
-Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
+Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+repeat red; intros; f_equal; auto.
 Qed.
 
 Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x.
-Proof. 
+Proof.
 intros; apply filter_b; auto.
 Qed.
 
-Lemma for_all_filter: 
+Lemma for_all_filter:
  forall s, for_all f s=is_empty (filter (fun x => negb (f x)) s).
-Proof. 
+Proof.
 intros; apply bool_1; split; intros.
 apply is_empty_1.
-unfold Empty; intros. 
+unfold Empty; intros.
 rewrite filter_iff; auto.
 red; destruct 1.
 rewrite <- (@for_all_iff s f) in H; auto.
@@ -621,10 +621,10 @@ rewrite filter_iff; auto.
 destruct (f x); auto.
 Qed.
 
-Lemma exists_filter : 
+Lemma exists_filter :
  forall s, exists_ f s=negb (is_empty (filter f s)).
-Proof. 
-intros; apply bool_1; split; intros. 
+Proof.
+intros; apply bool_1; split; intros.
 destruct (exists_2 Comp H) as (a,(Ha1,Ha2)).
 apply bool_6.
 red; intros; apply (@is_empty_2 _ H0 a); auto with set.
@@ -636,28 +636,28 @@ intros _ H0.
 rewrite (is_empty_1 (H0 (refl_equal None))) in H; auto; discriminate.
 Qed.
 
-Lemma partition_filter_1: 
+Lemma partition_filter_1:
  forall s, equal (fst (partition f s)) (filter f s)=true.
-Proof. 
+Proof.
 auto with set.
 Qed.
 
-Lemma partition_filter_2: 
+Lemma partition_filter_2:
  forall s, equal (snd (partition f s)) (filter (fun x => negb (f x)) s)=true.
-Proof. 
+Proof.
 auto with set.
 Qed.
 
-Lemma filter_add_1 : forall s x, f x = true -> 
- filter f (add x s) [=] add x (filter f s). 
+Lemma filter_add_1 : forall s x, f x = true ->
+ filter f (add x s) [=] add x (filter f s).
 Proof.
 red; intros; set_iff; do 2 (rewrite filter_iff; auto); set_iff.
 intuition.
 rewrite <- H; apply Comp; auto.
 Qed.
 
-Lemma filter_add_2 : forall s x, f x = false -> 
- filter f (add x s) [=] filter f s. 
+Lemma filter_add_2 : forall s x, f x = false ->
+ filter f (add x s) [=] filter f s.
 Proof.
 red; intros; do 2 (rewrite filter_iff; auto); set_iff.
 intuition.
@@ -665,18 +665,18 @@ assert (f x = f a) by (apply Comp; auto).
 rewrite H in H1; rewrite H2 in H1; discriminate.
 Qed.
 
-Lemma add_filter_1 : forall s s' x, 
+Lemma add_filter_1 : forall s s' x,
  f x=true -> (Add x s s') -> (Add x (filter f s) (filter f s')).
 Proof.
 unfold Add, MP.Add; intros.
 repeat rewrite filter_iff; auto.
 rewrite H0; clear H0.
-assert (E.eq x y -> f y = true) by 
+assert (E.eq x y -> f y = true) by
  (intro H0; rewrite <- (Comp _ _ H0); auto).
 tauto.
 Qed.
 
-Lemma add_filter_2 : forall s s' x, 
+Lemma add_filter_2 : forall s s' x,
  f x=false -> (Add x s s') -> filter f s [=] filter f s'.
 Proof.
 unfold Add, MP.Add, Equal; intros.
@@ -686,7 +686,7 @@ assert (f a = true -> ~E.eq x a).
  intros H0 H1.
  rewrite (Comp _ _ H1) in H.
  rewrite H in H0; discriminate.
-tauto. 
+tauto.
 Qed.
 
 Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) ->
@@ -695,7 +695,7 @@ Proof.
 clear Comp' Comp f.
 intros.
 assert (compat_bool E.eq (fun x => orb (f x) (g x))).
-  unfold compat_bool; intros.
+  unfold compat_bool, Proper, respectful; intros.
   rewrite (H x y H1);  rewrite (H0 x y H1); auto.
 unfold Equal; intros; set_iff; repeat rewrite filter_iff; auto.
 assert (f a || g a = true <-> f a = true \/ g a = true).
@@ -711,7 +711,7 @@ Qed.
 
 (** Properties of [for_all] *)
 
-Lemma for_all_mem_1: forall s, 
+Lemma for_all_mem_1: forall s,
  (forall x, (mem x s)=true->(f x)=true) -> (for_all f s)=true.
 Proof.
 intros.
@@ -724,8 +724,8 @@ generalize (H a); case (mem a s);intros;auto.
 rewrite H0;auto.
 Qed.
 
-Lemma for_all_mem_2: forall s, 
- (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true. 
+Lemma for_all_mem_2: forall s,
+ (for_all f s)=true -> forall x,(mem x s)=true -> (f x)=true.
 Proof.
 intros.
 rewrite for_all_filter in H; auto.
@@ -734,10 +734,10 @@ generalize (equal_mem_2 _ _ H x).
 rewrite filter_b; auto.
 rewrite empty_mem.
 rewrite H0; simpl;intros.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite <- negb_false_iff; auto.
 Qed.
 
-Lemma for_all_mem_3: 
+Lemma for_all_mem_3:
  forall s x,(mem x s)=true -> (f x)=false -> (for_all f s)=false.
 Proof.
 intros.
@@ -752,7 +752,7 @@ rewrite H0.
 simpl;auto.
 Qed.
 
-Lemma for_all_mem_4: 
+Lemma for_all_mem_4:
  forall s, for_all f s=false -> {x:elt | mem x s=true /\ f x=false}.
 Proof.
 intros.
@@ -762,12 +762,12 @@ exists x.
 rewrite filter_b in H1; auto.
 elim (andb_prop _ _ H1).
 split;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <- negb_true_iff; auto.
 Qed.
 
 (** Properties of [exists] *)
 
-Lemma for_all_exists: 
+Lemma for_all_exists:
  forall s, exists_ f s = negb (for_all (fun x =>negb (f x)) s).
 Proof.
 intros.
@@ -785,49 +785,49 @@ Variable Comp: compat_bool E.eq f.
 
 Let Comp' : compat_bool E.eq (fun x =>negb (f x)).
 Proof.
-unfold compat_bool in *; intros; f_equal; auto.
+unfold compat_bool, Proper, respectful in *; intros; f_equal; auto.
 Qed.
 
-Lemma exists_mem_1: 
+Lemma exists_mem_1:
  forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false.
 Proof.
 intros.
 rewrite for_all_exists; auto.
 rewrite for_all_mem_1;auto with bool.
-intros;generalize (H x H0);intros. 
-symmetry;apply negb_sym;simpl;auto.
+intros;generalize (H x H0);intros.
+rewrite negb_true_iff; auto.
 Qed.
 
-Lemma exists_mem_2: 
- forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false. 
+Lemma exists_mem_2:
+ forall s, exists_ f s=false -> forall x, mem x s=true -> f x=false.
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-replace false with (negb true);auto;apply negb_sym;symmetry.
-rewrite (for_all_mem_2 (fun x => negb (f x)) Comp' s);simpl;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
+rewrite negb_false_iff in H.
+rewrite <- negb_true_iff.
+apply for_all_mem_2 with (2:=H); auto.
 Qed.
 
-Lemma exists_mem_3: 
+Lemma exists_mem_3:
  forall s x, mem x s=true -> f x=true -> exists_ f s=true.
 Proof.
 intros.
 rewrite for_all_exists; auto.
-symmetry;apply negb_sym;simpl.
+rewrite negb_true_iff.
 apply for_all_mem_3 with x;auto.
-rewrite H0;auto.
+rewrite negb_false_iff; auto.
 Qed.
 
-Lemma exists_mem_4: 
+Lemma exists_mem_4:
  forall s, exists_ f s=true -> {x:elt | (mem x s)=true /\ (f x)=true}.
 Proof.
 intros.
 rewrite for_all_exists in H; auto.
-elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros.
+rewrite negb_true_iff in H.
+elim (for_all_mem_4 (fun x =>negb (f x)) Comp' s);intros;auto.
 elim p;intros.
 exists x;split;auto.
-replace true with (negb false);auto;apply negb_sym;auto.
-replace false with (negb true);auto;apply negb_sym;auto.
+rewrite <-negb_false_iff; auto.
 Qed.
 
 End Bool'.
@@ -836,21 +836,21 @@ Section Sum.
 
 (** Adding a valuation function on all elements of a set. *)
 
-Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0. 
-Notation compat_opL := (compat_op E.eq (@Logic.eq _)).
-Notation transposeL := (transpose (@Logic.eq _)).
+Definition sum (f:elt -> nat)(s:t) := fold (fun x => plus (f x)) s 0.
+Notation compat_opL := (compat_op E.eq Logic.eq).
+Notation transposeL := (transpose Logic.eq).
 
-Lemma sum_plus : 
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+Lemma sum_plus :
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
     forall s, sum (fun x =>f x+g x) s = sum f s + sum g s.
 Proof.
 unfold sum.
 intros f g Hf Hg.
-assert (fc : compat_opL (fun x:elt =>plus (f x))).  auto.
+assert (fc : compat_opL (fun x:elt =>plus (f x))).  red; auto.
 assert (ft : transposeL (fun x:elt =>plus (f x))). red; intros; omega.
-assert (gc : compat_opL (fun x:elt => plus (g x))). auto.
+assert (gc : compat_opL (fun x:elt => plus (g x))). red; auto.
 assert (gt : transposeL (fun x:elt =>plus (g x))). red; intros; omega.
-assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). auto.
+assert (fgc : compat_opL (fun x:elt =>plus ((f x)+(g x)))). repeat red; auto.
 assert (fgt : transposeL (fun x:elt=>plus ((f x)+(g x)))). red; intros; omega.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
 intros s;pattern s; apply set_rec.
@@ -863,14 +863,14 @@ rewrite H0;simpl;omega.
 do 3 rewrite fold_empty;auto.
 Qed.
 
-Lemma sum_filter : forall f, (compat_bool E.eq f) -> 
+Lemma sum_filter : forall f, (compat_bool E.eq f) ->
   forall s, (sum (fun x => if f x then 1 else 0) s) = (cardinal (filter f s)).
 Proof.
 unfold sum; intros f Hf.
 assert (st : Equivalence (@Logic.eq nat)) by (split; congruence).
-assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))). 
- red; intros.
- rewrite (Hf x x' H); auto.
+assert (cc : compat_opL (fun x => plus (if f x then 1 else 0))).
+ repeat red; intros.
+ rewrite (Hf _ _ H); auto.
 assert (ct : transposeL (fun x => plus (if f x then 1 else 0))).
  red; intros; omega.
 intros s;pattern s; apply set_rec.
@@ -891,12 +891,12 @@ unfold Empty; intros.
 rewrite filter_iff; auto; set_iff; tauto.
 Qed.
 
-Lemma fold_compat : 
+Lemma fold_compat :
   forall (A:Type)(eqA:A->A->Prop)(st:Equivalence eqA)
   (f g:elt->A->A),
-  (compat_op E.eq eqA f) -> (transpose eqA f) -> 
-  (compat_op E.eq eqA g) -> (transpose eqA g) -> 
-  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) -> 
+  (compat_op E.eq eqA f) -> (transpose eqA f) ->
+  (compat_op E.eq eqA g) -> (transpose eqA g) ->
+  forall (i:A)(s:t),(forall x:elt, (In x s) -> forall y, (eqA (f x y) (g x y))) ->
   (eqA (fold f s i) (fold g s i)).
 Proof.
 intros A eqA st f g fc ft gc gt i.
@@ -912,17 +912,18 @@ transitivity (f x (fold f s0 i)).
 apply fold_add with (eqA:=eqA); auto with set.
 transitivity (g x (fold f s0 i)); auto with set.
 transitivity (g x (fold g s0 i)); auto with set.
+apply gc; auto with *.
 symmetry; apply fold_add with (eqA:=eqA); auto.
 do 2 rewrite fold_empty; reflexivity.
 Qed.
 
-Lemma sum_compat : 
-  forall f g, compat_nat E.eq f -> compat_nat E.eq g -> 
+Lemma sum_compat :
+  forall f g, Proper (E.eq==>Logic.eq) f -> Proper (E.eq==>Logic.eq) g ->
   forall s, (forall x, In x s -> f x=g x) -> sum f s=sum g s.
 intros.
-unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto.
-red; intros; omega.
-red; intros; omega.
+unfold sum; apply (fold_compat _ (@Logic.eq nat)); auto with *.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
+intros x x' Hx y y' Hy. rewrite Hx, Hy; auto.
 Qed.
 
 End Sum.