FSetPositive: sets of positive inspired by FMapPositive.

 Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.

 I've also included a MSets version, hence FSetPositive might become
 soon a mere wrapper for MSetPositive, as for other FSets
 implementations.

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

9 files changed, 2426 insertions, 95 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 8f80d56ce..a4feb012b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -425,6 +425,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetWeakList.v
     theories/MSets/MSetList.v
     theories/MSets/MSetAVL.v
+    theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
   </dd>
@@ -444,8 +445,9 @@ through the <tt>Require Import</tt> command.</p>
     theories/FSets/FSetList.v
     theories/FSets/FSetWeakList.v
     theories/FSets/FSetCompat.v
-    (theories/FSets/FSets.v)
     theories/FSets/FSetAVL.v
+    theories/FSets/FSetPositive.v
+    (theories/FSets/FSets.v)
     theories/FSets/FSetToFiniteSet.v
     theories/FSets/FMapInterface.v
     theories/FSets/FMapWeakList.v
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index e85cc283e..c81a72f89 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -8,15 +8,14 @@
 
 (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *)
 
-Require Import Bool.
-Require Import ZArith.
-Require Import OrderedType.
-Require Import OrderedTypeEx.
-Require Import FMapInterface.
+Require Import Bool ZArith OrderedType OrderedTypeEx FMapInterface.
 
 Set Implicit Arguments.
 Open Local Scope positive_scope.
 
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+
 (** This file is an adaptation to the [FMap] framework of a work by
   Xavier Leroy and Sandrine Blazy (used for building certified compilers).
   Keys are of type [positive], and maps are binary trees: the sequence
@@ -25,95 +24,7 @@ Open Local Scope positive_scope.
   compression is implemented, and that the current file is simple enough to be
   self-contained. *)
 
-(** Even if [positive] can be seen as an ordered type with respect to the
-  usual order (see [OrderedTypeEx]), we use here a lexicographic order
-  over bits, which is more natural here (lower bits are considered first). *)
-
-Module PositiveOrderedTypeBits <: UsualOrderedType.
-  Definition t:=positive.
-  Definition eq:=@eq positive.
-  Definition eq_refl := @refl_equal t.
-  Definition eq_sym := @sym_eq t.
-  Definition eq_trans := @trans_eq t.
-
-  Fixpoint bits_lt (p q:positive) : Prop :=
-   match p, q with
-   | xH, xI _ => True
-   | xH, _ => False
-   | xO p, xO q => bits_lt p q
-   | xO _, _ => True
-   | xI p, xI q => bits_lt p q
-   | xI _, _ => False
-   end.
-
-  Definition lt:=bits_lt.
-
-  Lemma bits_lt_trans : forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
-  Proof.
-  induction x.
-  induction y; destruct z; simpl; eauto; intuition.
-  induction y; destruct z; simpl; eauto; intuition.
-  induction y; destruct z; simpl; eauto; intuition.
-  Qed.
-
-  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
-  Proof.
-  exact bits_lt_trans.
-  Qed.
-
-  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
-  Proof.
-  induction x; simpl; auto.
-  Qed.
-
-  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
-  Proof.
-  intros; intro.
-  rewrite <- H0 in H; clear H0 y.
-  unfold lt in H.
-  exact (bits_lt_antirefl x H).
-  Qed.
-
-  Definition compare : forall x y : t, Compare lt eq x y.
-  Proof.
-  induction x; destruct y.
-  (* I I *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* I O *)
-  apply GT; simpl; auto.
-  (* I H *)
-  apply GT; simpl; auto.
-  (* O I *)
-  apply LT; simpl; auto.
-  (* O O *)
-  destruct (IHx y).
-  apply LT; auto.
-  apply EQ; rewrite e; red; auto.
-  apply GT; auto.
-  (* O H *)
-  apply LT; simpl; auto.
-  (* H I *)
-  apply LT; simpl; auto.
-  (* H O *)
-  apply GT; simpl; auto.
-  (* H H *)
-  apply EQ; red; auto.
-  Qed.
-
-  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
-  Proof.
-  intros. case_eq ((x ?= y) Eq); intros.
-  left. apply Pcompare_Eq_eq; auto.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
-  Qed.
-
-End PositiveOrderedTypeBits.
-
-(** Other positive stuff *)
+(** First, some stuff about [positive] *)
 
 Fixpoint append (i j : positive) : positive :=
     match i with
@@ -166,6 +77,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
     | Leaf : tree A
     | Node : tree A -> option A -> tree A -> tree A.
 
+  Scheme tree_ind := Induction for tree Sort Prop.
+
   Definition t := tree.
 
   Section A.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
new file mode 100644
index 000000000..e5d55ac5b
--- /dev/null
+++ b/theories/FSets/FSetPositive.v
@@ -0,0 +1,1173 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(** Efficient implementation of [FSetInterface.S] for positive keys,
+    inspired from the [FMapPositive] module.
+
+   This module was adapted by Alexandre Ren, Damien Pous, and Thomas
+   Braibant (2010, LIG, CNRS, UMR 5217), from the [FMapPositive]
+   module of Pierre Letouzey and Jean-Christophe Filliâtre, which in
+   turn comes from the [FMap] framework of a work by Xavier Leroy and
+   Sandrine Blazy (used for building certified compilers).
+*)
+
+Require Import Bool BinPos OrderedType OrderedTypeEx FSetInterface.
+
+Set Implicit Arguments.
+
+Local Open Scope lazy_bool_scope.
+Local Open Scope positive_scope.
+
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+Local Unset Boolean Equality Schemes.
+
+
+Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
+
+  Module E:=PositiveOrderedTypeBits.
+
+  Definition elt := positive.
+
+  Inductive tree :=
+    | Leaf : tree
+    | Node : tree -> bool -> tree -> tree.
+
+  Scheme tree_ind := Induction for tree Sort Prop.
+
+  Definition t := tree.
+
+  Definition empty := Leaf.
+
+  Fixpoint is_empty (m : t) : bool :=
+   match m with
+    | Leaf => true
+    | Node l b r => negb b &&& is_empty l &&& is_empty r
+   end.
+
+  Fixpoint mem (i : positive) (m : t) : bool :=
+    match m with
+    | Leaf => false
+    | Node l o r =>
+        match i with
+        | 1 => o
+        | i~0 => mem i l
+        | i~1 => mem i r
+        end
+    end.
+
+  Fixpoint add (i : positive) (m : t) : t :=
+    match m with
+    | Leaf =>
+        match i with
+        | 1 => Node Leaf true Leaf
+        | i~0 => Node (add i Leaf) false Leaf
+        | i~1 => Node Leaf false (add i Leaf)
+        end
+    | Node l o r =>
+        match i with
+        | 1 => Node l true r
+        | i~0 => Node (add i l) o r
+        | i~1 => Node l o (add i r)
+        end
+    end.
+
+  Definition singleton i := add i empty.
+
+  (** helper function to avoid creating empty trees that are not leaves *)
+
+  Definition node l (b: bool) r :=
+    if b then Node l b r else
+     match l,r with
+       | Leaf,Leaf => Leaf
+       | _,_ => Node l false r end.
+
+  Fixpoint remove (i : positive) (m : t) : t :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match i with
+          | 1 => node l false r
+          | i~0 => node (remove i l) o r
+          | i~1 => node l o (remove i r)
+        end
+    end.
+
+  Fixpoint union (m m': t) :=
+    match m with
+      | Leaf => m'
+      | Node l o r =>
+        match m' with
+          | Leaf => m
+          | Node l' o' r' => Node (union l l') (o||o') (union r r')
+        end
+    end.
+
+  Fixpoint inter (m m': t) :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match m' with
+          | Leaf => Leaf
+          | Node l' o' r' => node (inter l l') (o&&o') (inter r r')
+        end
+    end.
+
+  Fixpoint diff (m m': t) :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match m' with
+          | Leaf => m
+          | Node l' o' r' => node (diff l l') (o&&negb o') (diff r r')
+        end
+    end.
+
+  Fixpoint equal (m m': t): bool :=
+    match m with
+      | Leaf => is_empty m'
+      | Node l o r =>
+        match m' with
+          | Leaf => is_empty m
+          | Node l' o' r' => eqb o o' &&& equal l l' &&& equal r r'
+        end
+    end.
+
+  Fixpoint subset (m m': t): bool :=
+    match m with
+      | Leaf => true
+      | Node l o r =>
+        match m' with
+          | Leaf => is_empty m
+          | Node l' o' r' => (negb o ||| o') &&& subset l l' &&& subset r r'
+        end
+    end.
+
+  (** reverses [y] and concatenate it with [x] *)
+
+  Fixpoint rev_append y x :=
+    match y with
+      | 1 => x
+      | y~1 => rev_append y x~1
+      | y~0 => rev_append y x~0
+    end.
+  Infix "@" := rev_append (at level 60).
+  Definition rev x := x@1.
+
+  Section Fold.
+
+    Variables B : Type.
+    Variable f : positive -> B -> B.
+
+    (** the additional argument, [i], records the current path, in
+       reverse order (this should be more efficient: we reverse this argument
+       only at present nodes only, rather than at each node of the tree).
+       we also use this convention in all functions below
+     *)
+
+    Fixpoint xfold (m : t) (v : B) (i : positive) :=
+      match m with
+        | Leaf => v
+        | Node l true r =>
+          xfold r (f (rev i) (xfold l v i~0)) i~1
+        | Node l false r =>
+          xfold r (xfold l v i~0) i~1
+      end.
+    Definition fold m i := xfold m i 1.
+
+  End Fold.
+
+  Section Quantifiers.
+
+    Variable f : positive -> bool.
+
+    Fixpoint xforall (m : t) (i : positive) :=
+      match m with
+        | Leaf => true
+        | Node l o r =>
+          (negb o ||| f (rev i)) &&& xforall r i~1 &&& xforall l i~0
+      end.
+    Definition for_all m := xforall m 1.
+
+    Fixpoint xexists (m : t) (i : positive) :=
+      match m with
+        | Leaf => false
+        | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
+      end.
+    Definition exists_ m := xexists m 1.
+
+    Fixpoint xfilter (m : t) (i : positive) :=
+      match m with
+        | Leaf => Leaf
+        | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
+      end.
+    Definition filter m := xfilter m 1.
+
+    Fixpoint xpartition (m : t) (i : positive) :=
+      match m with
+        | Leaf => (Leaf,Leaf)
+        | Node l o r =>
+          let (lt,lf) := xpartition l i~0 in
+          let (rt,rf) := xpartition r i~1 in
+             if o then
+               let fi := f (rev i) in
+                 (node lt fi rt, node lf (negb fi) rf)
+             else
+                 (node lt false rt, node lf false rf)
+      end.
+    Definition partition m := xpartition m 1.
+
+  End Quantifiers.
+
+  (** uses [a] to accumulate values rather than doing a lot of concatenations *)
+
+  Fixpoint xelements (m : t) (i : positive) (a: list positive) :=
+    match m with
+      | Leaf => a
+      | Node l false r => xelements l i~0 (xelements r i~1 a)
+      | Node l true r => xelements l i~0 (rev i :: xelements r i~1 a)
+    end.
+
+  Definition elements (m : t) := xelements m 1 nil.
+
+  Fixpoint cardinal (m : t) : nat :=
+    match m with
+      | Leaf => O
+      | Node l false r => (cardinal l + cardinal r)%nat
+      | Node l true r => S (cardinal l + cardinal r)
+    end.
+
+  Definition omap (f: elt -> elt) x :=
+    match x with
+      | None => None
+      | Some i => Some (f i)
+    end.
+
+  (** would it be more efficient to use a path like in the above functions ? *)
+
+  Fixpoint choose (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r => if o then Some 1 else
+        match choose l with
+          | None => omap xI (choose r)
+          | Some i => Some i~0
+        end
+    end.
+
+  Fixpoint min_elt (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r =>
+        match min_elt l with
+          | None => if o then Some 1 else omap xI (min_elt r)
+          | Some i => Some i~0
+        end
+    end.
+
+  Fixpoint max_elt (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r =>
+        match max_elt r with
+          | None => if o then Some 1 else omap xO (max_elt l)
+          | Some i => Some i~1
+        end
+    end.
+
+  (** lexicographic product, defined using a notation to keep things lazy *)
+
+  Notation lex u v := match u with Eq => v | Lt => Lt | Gt => Gt end.
+
+  Definition compare_bool a b :=
+    match a,b with
+      | false, true => Lt
+      | true, false => Gt
+      | _,_ => Eq
+    end.
+
+  Fixpoint compare_fun (m m': t): comparison :=
+    match m,m' with
+      | Leaf,_ => if is_empty m' then Eq else Lt
+      | _,Leaf => if is_empty m then Eq else Gt
+      | Node l o r,Node l' o' r' =>
+        lex (compare_bool o o') (lex (compare_fun l l') (compare_fun r r'))
+    end.
+
+
+  Definition In i t := mem i t = true.
+  Definition Equal s s' := forall a : elt, In a  s <-> In a  s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+  Notation "s  [=]  t" := (Equal s t) (at level 70, no associativity).
+  Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
+
+  Definition eq := Equal.
+  Definition lt m m' := compare_fun m m' = Lt.
+
+  (** Specification of [In] *)
+
+  Lemma In_1: forall s x y, E.eq x y -> In x s -> In y s.
+  Proof. intros s x y ->. trivial. Qed.
+
+  (** Specification of [eq] *)
+
+  Lemma eq_refl: forall s, eq s s.
+  Proof. unfold eq, Equal. reflexivity. Qed.
+
+  Lemma eq_sym: forall s s', eq s s' -> eq s' s.
+  Proof. unfold eq, Equal. intros. symmetry. trivial. Qed.
+
+  Lemma eq_trans: forall s s' s'', eq s s' -> eq s' s'' -> eq s s''.
+  Proof. unfold eq, Equal. intros ? ? ? H ? ?. rewrite H. trivial. Qed.
+
+  (** Specification of [mem] *)
+
+  Lemma mem_1: forall s x, In x s -> mem x s = true.
+  Proof. unfold In. trivial. Qed.
+
+  Lemma mem_2: forall s x, mem x s = true -> In x s.
+  Proof. unfold In. trivial. Qed.
+
+  (** Additional lemmas for mem  *)
+
+  Lemma mem_Leaf: forall x, mem x Leaf = false.
+  Proof. destruct x; trivial. Qed.
+
+  (** Specification of [empty] *)
+
+  Lemma empty_1 : Empty empty.
+  Proof. unfold Empty, In. intro. rewrite mem_Leaf. discriminate. Qed.
+
+  (** Specification of node  *)
+
+  Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r).
+  Proof.
+    intros x l o r.
+    case o; trivial.
+    destruct l; trivial.
+    destruct r; trivial.
+    symmetry. destruct x.
+      apply mem_Leaf.
+      apply mem_Leaf.
+      reflexivity.
+  Qed.
+  Local Opaque node.
+
+  (** Specification of [is_empty] *)
+
+  Lemma is_empty_spec: forall s, Empty s <-> is_empty s = true.
+  Proof.
+    unfold Empty, In.
+    induction s as [|l IHl o r IHr]; simpl.
+      setoid_rewrite mem_Leaf. firstorder.
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear IHl IHr.
+      destruct o; simpl; split.
+        intro H. elim (H 1). reflexivity.
+        intuition discriminate.
+        intro H. split. split. reflexivity.
+          intro a. apply (H a~0).
+          intro a. apply (H a~1).
+        intros H [a|a|]; apply H || intro; discriminate.
+  Qed.
+
+  Lemma is_empty_1: forall s, Empty s -> is_empty s = true.
+  Proof. intro. rewrite is_empty_spec. trivial. Qed.
+
+  Lemma is_empty_2: forall s, is_empty s = true -> Empty s.
+  Proof. intro. rewrite is_empty_spec. trivial. Qed.
+
+  (** Specification of [subset] *)
+
+  Lemma subset_Leaf_s: forall s, Leaf [<=] s.
+  Proof. intros s i Hi. elim (empty_1 Hi). Qed.
+
+  Lemma subset_spec: forall s s', s [<=] s' <-> subset s s' = true.
+  Proof.
+    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl.
+      split; intros. reflexivity. apply subset_Leaf_s.
+
+      split; intros. reflexivity. apply subset_Leaf_s.
+
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- 2is_empty_spec.
+      destruct o; simpl.
+        split.
+          intro H. elim (@empty_1 1). apply H. reflexivity.
+          intuition discriminate.
+        split; intro H.
+          split. split. reflexivity.
+          unfold Empty. intros a H1. apply (@empty_1 (a~0)). apply H. assumption.
+          unfold Empty. intros a H1. apply (@empty_1 (a~1)). apply H. assumption.
+          destruct H as [[_ Hl] Hr].
+          intros [i|i|] Hi.
+            elim (Hr i Hi).
+            elim (Hl i Hi).
+            discriminate.
+
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, <- IHl, <- IHr. clear.
+      destruct o; simpl.
+       split; intro H.
+         split. split.
+          destruct o'; trivial.
+          specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity.
+          intros i Hi. apply (H i~0). apply Hi.
+          intros i Hi. apply (H i~1). apply Hi.
+         destruct H as [[Ho' Hl] Hr]. rewrite Ho'.
+          intros i Hi. destruct i.
+            apply (Hr i). assumption.
+            apply (Hl i). assumption.
+            assumption.
+       split; intros.
+         split. split. reflexivity.
+           intros i Hi. apply (H i~0). apply Hi.
+           intros i Hi. apply (H i~1). apply Hi.
+           intros i Hi. destruct i; destruct H as [[H Hl] Hr].
+             apply (Hr i). assumption.
+             apply (Hl i). assumption.
+             discriminate Hi.
+  Qed.
+
+
+  Lemma subset_1: forall s s', Subset s s' -> subset s s' = true.
+  Proof. intros s s'. apply -> subset_spec; trivial. Qed.
+
+  Lemma subset_2: forall s s', subset s s' = true -> Subset s s'.
+  Proof. intros s s'. apply <- subset_spec; trivial. Qed.
+
+  (** Specification of [equal] (via subset) *)
+
+  Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s.
+  Proof.
+    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial.
+      destruct o. reflexivity. rewrite andb_comm. reflexivity.
+      rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true.
+       rewrite 7andb_true_iff, eqb_true_iff.
+      rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst.
+       destruct o'; reflexivity.
+       destruct o'; reflexivity.
+       destruct o; auto. destruct o'; trivial.
+  Qed.
+
+  Lemma equal_spec: forall s s', Equal s s' <-> equal s s' = true.
+  Proof.
+    intros. rewrite equal_subset. rewrite andb_true_iff.
+    rewrite <- 2subset_spec. unfold Equal, Subset. firstorder.
+  Qed.
+
+  Lemma equal_1: forall s s', Equal s s' -> equal s s' = true.
+  Proof. intros s s'. apply -> equal_spec; trivial. Qed.
+
+  Lemma equal_2: forall s s', equal s s' = true -> Equal s s'.
+  Proof. intros s s'. apply <- equal_spec; trivial. Qed.
+
+  Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
+  Proof.
+    unfold eq.
+    intros. case_eq (equal s s'); intro H.
+     left. apply equal_2, H.
+     right. abstract (intro H'; rewrite (equal_1 H') in H; discriminate).
+  Defined.
+
+  (** (Specified) definition of [compare] *)
+
+  Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' ->
+    lex u v = CompOpp (lex u' v').
+  Proof. intros ? ? u' ? -> ->. case u'; reflexivity. Qed.
+
+  Lemma compare_bool_inv: forall b b',
+    compare_bool b b' = CompOpp (compare_bool b' b).
+  Proof. intros [|] [|]; reflexivity. Qed.
+
+  Lemma compare_inv: forall s s', compare_fun s s' = CompOpp (compare_fun s' s).
+  Proof.
+    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial.
+    unfold compare_fun. case is_empty; reflexivity.
+    unfold compare_fun. case is_empty; reflexivity.
+    simpl. rewrite compare_bool_inv.
+     case compare_bool; simpl; trivial; apply lex_Opp; auto.
+  Qed.
+
+  Lemma lex_Eq: forall u v, lex u v = Eq <-> u=Eq /\ v=Eq.
+  Proof. intros u v; destruct u; intuition discriminate. Qed.
+
+  Lemma compare_bool_Eq: forall b1 b2,
+    compare_bool b1 b2 = Eq <-> eqb b1 b2 = true.
+  Proof. intros [|] [|]; intuition discriminate. Qed.
+
+  Lemma compare_equal: forall s s', compare_fun s s' = Eq <-> equal s s' = true.
+  Proof.
+    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r'].
+     simpl. tauto.
+     unfold compare_fun, equal. case is_empty; intuition discriminate.
+     unfold compare_fun, equal. case is_empty; intuition discriminate.
+     simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff.
+     rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr.
+     rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity.
+  Qed.
+
+
+  Lemma compare_gt: forall s s', compare_fun s s' = Gt -> lt s' s.
+  Proof.
+    unfold lt. intros s s'. rewrite compare_inv.
+     case compare_fun; trivial; intros; discriminate.
+  Qed.
+
+  Lemma compare_eq: forall s s', compare_fun s s' = Eq -> eq s s'.
+  Proof.
+    unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial.
+  Qed.
+
+  Lemma compare : forall s s' : t, Compare lt eq s s'.
+  Proof.
+    intros. case_eq (compare_fun s s'); intro H.
+    apply EQ. apply compare_eq, H.
+    apply LT. assumption.
+    apply GT. apply compare_gt, H.
+  Defined.
+
+  Section lt_spec.
+
+  Inductive ct: comparison -> comparison -> comparison -> Prop :=
+  | ct_xxx: forall x, ct x  x  x
+  | ct_xex: forall x, ct x  Eq x
+  | ct_exx: forall x, ct Eq x  x
+  | ct_glx: forall x, ct Gt Lt x
+  | ct_lgx: forall x, ct Lt Gt x.
+
+  Lemma ct_cxe: forall x, ct (CompOpp x) x Eq.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xce: forall x, ct x (CompOpp x) Eq.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_lxl: forall x, ct Lt x Lt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_gxg: forall x, ct Gt x Gt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xll: forall x, ct x Lt Lt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xgg: forall x, ct x Gt Gt.
+  Proof. destruct x; constructor. Qed.
+
+  Local Hint Constructors ct: ct.
+  Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg: ct.
+  Ltac ct := trivial with ct.
+
+  Lemma ct_lex: forall u v w u' v' w',
+    ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w').
+  Proof.
+    intros u v w u' v' w' H H'.
+    inversion_clear H; inversion_clear H'; ct; destruct w; ct; destruct w'; ct.
+  Qed.
+
+  Lemma ct_compare_bool:
+    forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c).
+  Proof.
+    intros [|] [|] [|]; constructor.
+  Qed.
+
+  Lemma compare_x_Leaf: forall s,
+    compare_fun s Leaf = if is_empty s then Eq else Gt.
+  Proof.
+    intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity.
+  Qed.
+
+  Lemma compare_empty_x: forall a, is_empty a = true ->
+    forall b, compare_fun a b = if is_empty b then Eq else Lt.
+  Proof.
+    induction a as [|l IHl o r IHr]; trivial.
+    destruct o. intro; discriminate.
+    simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff.
+    intros [Hl Hr].
+    destruct b as [|l' [|] r']; simpl compare_fun; trivial.
+     rewrite Hl, Hr. trivial.
+     rewrite (IHl Hl), (IHr Hr). simpl.
+     case (is_empty l'); case (is_empty r'); trivial.
+  Qed.
+
+  Lemma compare_x_empty: forall a, is_empty a = true ->
+    forall b, compare_fun b a = if is_empty b then Eq else Gt.
+  Proof.
+    setoid_rewrite <- compare_x_Leaf.
+    intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity.
+  Qed.
+
+  Lemma ct_compare_fun:
+    forall a b c, ct (compare_fun a b) (compare_fun b c) (compare_fun a c).
+  Proof.
+    induction a as [|l IHl o r IHr]; intros s' s''.
+     destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct.
+      rewrite compare_inv. ct.
+      unfold compare_fun at 1. case_eq (is_empty (Node l' o' r')); intro H'.
+       rewrite (compare_empty_x _ H'). ct.
+       unfold compare_fun at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''.
+        rewrite (compare_x_empty _ H''), H'. ct.
+        ct.
+
+     destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r''].
+      ct.
+      unfold compare_fun at 2. rewrite compare_x_Leaf.
+      case_eq (is_empty (Node l o r)); intro H.
+       rewrite (compare_empty_x _ H). ct.
+       case_eq (is_empty (Node l'' o'' r'')); intro H''.
+        rewrite (compare_x_empty _ H''), H. ct.
+        ct.
+
+      rewrite 2 compare_x_Leaf.
+      case_eq (is_empty (Node l o r)); intro H.
+       rewrite compare_inv, (compare_x_empty _ H). ct.
+       case_eq (is_empty (Node l' o' r')); intro H'.
+        rewrite (compare_x_empty _ H'), H. ct.
+        ct.
+
+      simpl compare_fun. apply ct_lex. apply ct_compare_bool.
+       apply ct_lex; trivial.
+  Qed.
+
+  End lt_spec.
+
+  Lemma lt_trans: forall s s' s'', lt s s' -> lt s' s'' -> lt s s''.
+  Proof.
+    unfold lt. intros a b c. assert (H := ct_compare_fun a b c).
+    inversion_clear H; trivial; intros; discriminate.
+  Qed.
+
+  Lemma lt_not_eq: forall s s', lt s s' -> ~ eq s s'.
+  Proof.
+    unfold lt, eq. intros s s' H H'.
+     rewrite equal_spec, <- compare_equal in H'. congruence.
+  Qed.
+
+  (** Specification of [add] *)
+
+  Lemma add_spec: forall x y s, In y (add x s) <-> x=y \/ In y s.
+  Proof.
+    unfold In. induction x; intros [y|y|] [|l o r]; simpl mem;
+    try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence.
+  Qed.
+
+  Lemma add_1: forall s x y, x = y -> In y (add x s).
+  Proof. intros. apply <- add_spec. left. assumption. Qed.
+
+  Lemma add_2: forall s x y, In y s -> In y (add x s).
+  Proof. intros. apply <- add_spec. right. assumption. Qed.
+
+  Lemma add_3: forall s x y, x<>y -> In y (add x s) -> In y s.
+  Proof.
+    intros s x y H. rewrite add_spec. intros [->|?]; trivial. elim H; trivial.
+  Qed.
+
+  (** Specification of [remove] *)
+
+  Lemma remove_spec: forall x y s, In y (remove x s) <-> x<>y /\ In y s.
+  Proof.
+    unfold In.
+    induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node;
+     simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf;
+     intuition congruence.
+  Qed.
+
+  Lemma remove_1: forall s x y, x=y -> ~ In y (remove x s).
+  Proof. intros. rewrite remove_spec. tauto. Qed.
+
+  Lemma remove_2: forall s x y, x<>y -> In y s -> In y (remove x s).
+  Proof. intros. rewrite remove_spec. split; assumption. Qed.
+
+  Lemma remove_3: forall s x y, In y (remove x s) -> In y s.
+  Proof. intros s x y. rewrite remove_spec. tauto. Qed.
+
+  (** Specification of [singleton] *)
+
+  Lemma singleton_1: forall x y, In y (singleton x) -> x=y.
+  Proof.
+    unfold singleton. intros x y. rewrite add_spec.
+    unfold In. rewrite mem_Leaf. intuition discriminate.
+  Qed.
+
+  Lemma singleton_2: forall x y, x = y -> In y (singleton x).
+  Proof.
+    unfold singleton. intros. apply add_1. assumption.
+  Qed.
+
+  (** Specification of [union] *)
+
+  Lemma union_spec: forall x s s', In x (union s s') <-> In x s \/ In x s'.
+  Proof.
+    unfold In.
+    induction x; destruct s; destruct s'; simpl union; simpl mem;
+      try (rewrite IHx; clear IHx); try intuition congruence.
+      apply orb_true_iff.
+  Qed.
+
+  Lemma union_1: forall s s' x, In x (union s s') -> In x s \/ In x s'.
+  Proof. intros. apply -> union_spec. assumption. Qed.
+
+  Lemma union_2: forall s s' x, In x s -> In x (union s s').
+  Proof. intros. apply <- union_spec. left. assumption. Qed.
+
+  Lemma union_3: forall s s' x, In x s' -> In x (union s s').
+  Proof. intros. apply <- union_spec. right. assumption. Qed.
+
+  (** Specification of [inter] *)
+
+  Lemma inter_spec: forall x s s', In x (inter s s') <-> In x s /\ In x s'.
+  Proof.
+    unfold In.
+    induction x; destruct s; destruct s'; simpl inter; rewrite ?mem_node;
+     simpl mem; try (rewrite IHx; clear IHx); try intuition congruence.
+     apply andb_true_iff.
+  Qed.
+
+  Lemma inter_1: forall s s' x, In x (inter s s') -> In x s.
+  Proof. intros s s' x. rewrite inter_spec. tauto. Qed.
+
+  Lemma inter_2: forall s s' x, In x (inter s s') -> In x s'.
+  Proof. intros s s' x. rewrite inter_spec. tauto. Qed.
+
+  Lemma inter_3: forall s s' x, In x s -> In x s' -> In x (inter s s').
+  Proof. intros. rewrite inter_spec. split; assumption. Qed.
+
+  (** Specification of [diff] *)
+
+  Lemma diff_spec: forall x s s', In x (diff s s') <-> In x s /\ ~ In x s'.
+  Proof.
+    unfold In.
+    induction x; destruct s; destruct s' as [|l' o' r']; simpl diff;
+     rewrite ?mem_node; simpl mem;
+      try (rewrite IHx; clear IHx); try intuition congruence.
+      rewrite andb_true_iff. destruct o'; intuition discriminate.
+  Qed.
+
+  Lemma diff_1: forall s s' x, In x (diff s s') -> In x s.
+  Proof. intros s s' x. rewrite diff_spec. tauto. Qed.
+
+  Lemma diff_2: forall s s' x, In x (diff s s') -> ~ In x s'.
+  Proof. intros s s' x. rewrite diff_spec. tauto. Qed.
+
+  Lemma diff_3: forall s s' x, In x s -> ~ In x s' -> In x (diff s s').
+  Proof. intros. rewrite diff_spec. split; assumption. Qed.
+
+  (** Specification of [fold] *)
+
+  Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+  Proof.
+    unfold fold, elements. intros s A i f. revert s i.
+    set (f' := fun a e => f e a).
+    assert (H: forall s i j acc,
+      fold_left f' acc (xfold f s i j) =
+      fold_left f' (xelements s j acc) i).
+
+    induction s as [|l IHl o r IHr]; intros; trivial.
+      destruct o; simpl xelements; simpl xfold.
+        rewrite IHr, <- IHl. reflexivity.
+        rewrite IHr. apply IHl.
+
+    intros. exact (H s i 1 nil).
+  Qed.
+
+  (** Specification of [cardinal] *)
+
+  Lemma cardinal_1: forall s, cardinal s = length (elements s).
+  Proof.
+    unfold elements.
+    assert (H: forall s j acc,
+                (cardinal s + length acc)%nat = length (xelements s j acc)).
+
+    induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b.
+      rewrite <- IHl. simpl. rewrite <- IHr.
+       rewrite <- plus_n_Sm, Plus.plus_assoc. reflexivity.
+      rewrite <- IHl, <- IHr. rewrite Plus.plus_assoc. reflexivity.
+
+    intros. rewrite <- H. simpl. rewrite Plus.plus_comm. reflexivity.
+  Qed.
+
+  (** Specification of [filter] *)
+
+  Lemma xfilter_spec: forall f s x i,
+    In x (xfilter f s i) <-> In x s /\ f (i@x) = true.
+  Proof.
+    intro f. unfold In.
+    induction s as [|l IHl o r IHr]; intros x i; simpl xfilter.
+     rewrite mem_Leaf. intuition discriminate.
+     rewrite mem_node. destruct x; simpl.
+       rewrite IHr. reflexivity.
+       rewrite IHl. reflexivity.
+       rewrite <- andb_lazy_alt. apply andb_true_iff.
+  Qed.
+
+  Lemma filter_1 : forall s x f, compat_bool E.eq f ->
+    In x (filter f s) -> In x s.
+  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
+
+  Lemma filter_2 : forall s x f, compat_bool E.eq f ->
+    In x (filter f s) -> f x = true.
+  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
+
+  Lemma filter_3 : forall s x f, compat_bool E.eq f -> In x s ->
+    f x = true -> In x (filter f s).
+  Proof. unfold filter. intros s x f _. rewrite xfilter_spec. tauto. Qed.
+
+
+  (** Specification of [for_all] *)
+
+  Lemma xforall_spec: forall f s i,
+    xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.
+  Proof.
+    unfold For_all, In. intro f.
+    induction s as [|l IHl o r IHr]; intros i; simpl.
+     setoid_rewrite mem_Leaf. intuition discriminate.
+     rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
+     rewrite IHl, IHr. clear IHl IHr.
+      split.
+       intros [[Hi Hr] Hl] x. destruct x; simpl; intro H.
+        apply Hr, H.
+        apply Hl, H.
+        rewrite H in Hi. assumption.
+       intro H; intuition.
+        specialize (H 1). destruct o. apply H. reflexivity. reflexivity.
+        apply H. assumption.
+        apply H. assumption.
+  Qed.
+
+  Lemma for_all_1 : forall s f, compat_bool E.eq f ->
+    For_all (fun x => f x = true) s -> for_all f s = true.
+  Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
+
+  Lemma for_all_2 : forall s f, compat_bool E.eq f ->
+    for_all f s = true -> For_all (fun x => f x = true) s.
+  Proof. intros s f _. unfold for_all. rewrite xforall_spec. trivial. Qed.
+
+
+  (** Specification of [exists] *)
+
+  Lemma xexists_spec: forall f s i,
+    xexists f s i = true <-> Exists (fun x => f (i@x) = true) s.
+  Proof.
+    unfold Exists, In. intro f.
+    induction s as [|l IHl o r IHr]; intros i; simpl.
+     setoid_rewrite mem_Leaf. firstorder.
+     rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
+     rewrite IHl, IHr. clear IHl IHr.
+      split.
+       intros [[Hi|[x Hr]]|[x Hl]].
+        exists 1. exact Hi.
+        exists x~1. exact Hr.
+        exists x~0. exact Hl.
+       intros [[x|x|] H]; eauto.
+  Qed.
+
+  Lemma exists_1 : forall s f, compat_bool E.eq f ->
+      Exists (fun x => f x = true) s -> exists_ f s = true.
+  Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
+
+  Lemma exists_2 : forall s f, compat_bool E.eq f ->
+      exists_ f s = true -> Exists (fun x => f x = true) s.
+  Proof. intros s f _. unfold exists_. rewrite xexists_spec. trivial. Qed.
+
+
+  (** Specification of [partition] *)
+
+  Lemma partition_filter : forall s f,
+    partition f s = (filter f s, filter (fun x => negb (f x)) s).
+  Proof.
+    unfold partition, filter. intros s f. generalize 1 as j.
+    induction s as [|l IHl o r IHr]; intro j.
+      reflexivity.
+      destruct o; simpl; rewrite IHl, IHr; reflexivity.
+  Qed.
+
+  Lemma partition_1 : forall s f, compat_bool E.eq f ->
+      Equal (fst (partition f s)) (filter f s).
+  Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
+
+  Lemma partition_2 : forall s f, compat_bool E.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof. intros. rewrite partition_filter. apply eq_refl. Qed.
+
+
+  (** Specification of [elements] *)
+
+  Notation InL := (InA E.eq).
+
+  Lemma xelements_spec: forall s j acc y,
+    InL y (xelements s j acc)
+    <->
+    InL y acc \/ exists x, y=(j@x) /\ mem x s = true.
+  Proof.
+    induction s as [|l IHl o r IHr]; simpl.
+      intros. split; intro H.
+        left. assumption.
+        destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_1 Hx').
+
+      intros j acc y. case o.
+        rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split.
+          intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto.
+            right. exists x~1. auto.
+            right. exists x~0. auto.
+          intros [H|[x [-> H]]].
+            eauto.
+            destruct x.
+              left. right. right. exists x; auto.
+              right. exists x; auto.
+              left. left. reflexivity.
+
+        rewrite IHl, IHr. clear IHl IHr. split.
+          intros [[H|[x [-> H]]]|[x [-> H]]].
+            eauto.
+            right. exists x~1. auto.
+            right. exists x~0. auto.
+          intros [H|[x [-> H]]].
+            eauto.
+            destruct x.
+              left. right.  exists x; auto.
+              right. exists x; auto.
+              discriminate.
+  Qed.
+
+  Lemma elements_1: forall s x, In x s -> InL x (elements s).
+  Proof.
+    unfold elements, In. intros.
+    rewrite xelements_spec. right. exists x. auto.
+  Qed.
+
+  Lemma elements_2: forall s x, InL x (elements s) -> In x s.
+  Proof.
+    unfold elements, In. intros s x H.
+    rewrite xelements_spec in H. destruct H as [H|[y [H H']]].
+      inversion_clear H.
+      rewrite H. assumption.
+  Qed.
+
+  Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y).
+  Proof. induction j; intros; simpl; auto. Qed.
+
+  Lemma elements_3: forall s, sort E.lt (elements s).
+  Proof.
+    unfold elements.
+    assert (H: forall s j acc,
+      sort E.lt acc ->
+      (forall x y, In x s ->  InL y acc -> E.lt (j@x) y) ->
+      sort E.lt (xelements s j acc)).
+
+    induction s as [|l IHl o r IHr]; simpl; trivial.
+    intros j acc Hacc Hsacc. destruct o.
+      apply IHl. constructor.
+       apply IHr. apply Hacc.
+       intros x y Hx Hy. apply Hsacc; assumption.
+       case_eq (xelements r j~1 acc). constructor.
+       intros z q H. constructor.
+       assert (H': InL z (xelements r j~1 acc)).
+        rewrite H. constructor. reflexivity.
+       clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]].
+         apply (Hsacc 1 z); trivial. reflexivity.
+         simpl. apply lt_rev_append. exact I.
+       intros x y Hx Hy. inversion_clear Hy.
+         rewrite H. simpl. apply lt_rev_append. exact I.
+         rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]].
+           apply Hsacc; assumption.
+           simpl. apply lt_rev_append. exact I.
+
+      apply IHl. apply IHr. apply Hacc.
+       intros x y Hx Hy. apply Hsacc; assumption.
+       intros x y Hx Hy. rewrite xelements_spec in Hy.
+        destruct Hy as [Hy|[z [-> Hy]]].
+         apply Hsacc; assumption.
+         simpl. apply lt_rev_append. exact I.
+
+    intros. apply H. constructor.
+      intros x y _ H'. inversion H'.
+  Qed.
+
+  Lemma elements_3w: forall s, NoDupA E.eq (elements s).
+  Proof.
+    intro. apply SortA_NoDupA with E.lt.
+      constructor.
+       intro. apply E.eq_refl.
+       intro. apply E.eq_sym.
+       intro. apply E.eq_trans.
+      constructor.
+       intros x H. apply E.lt_not_eq in H. apply H. reflexivity.
+       intro. apply E.lt_trans.
+      intros ? ? <- ? ? <-. reflexivity.
+      apply elements_3.
+  Qed.
+
+
+  (** Specification of [choose] *)
+
+  Lemma choose_1: forall s x, choose s = Some x -> In x s.
+  Proof.
+    induction s as [| l IHl o r IHr]; simpl.
+      intros. discriminate.
+      destruct o.
+        intros x H. injection H; intros; subst. reflexivity.
+        revert IHl. case choose.
+          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+           reflexivity.
+          intros _ x. revert IHr. case choose.
+            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            reflexivity.
+            intros. discriminate.
+  Qed.
+
+  Lemma choose_2: forall s, choose s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_1.
+      destruct o.
+        discriminate.
+        simpl in H. destruct (choose l).
+          discriminate.
+          destruct (choose r).
+            discriminate.
+            intros [a|a|].
+              apply IHr. reflexivity.
+              apply IHl. reflexivity.
+              discriminate.
+  Qed.
+
+  Lemma choose_empty: forall s, is_empty s = true -> choose s = None.
+  Proof.
+    intros s Hs. case_eq (choose s); trivial.
+    intros p Hp. apply choose_1 in Hp. apply is_empty_2 in Hs. elim (Hs _ Hp).
+  Qed.
+
+  Lemma choose_3': forall s s', Equal s s' -> choose s = choose s'.
+  Proof.
+    setoid_rewrite equal_spec.
+    induction s as [|l IHl o r IHr].
+      intros. symmetry. apply choose_empty. assumption.
+
+      destruct s' as [|l' o' r'].
+        generalize (Node l o r) as s. simpl. intros. apply choose_empty.
+        rewrite <- equal_spec in H. apply eq_sym in H. rewrite equal_spec in H.
+        assumption.
+
+        simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff.
+        intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity.
+  Qed.
+
+  Lemma choose_3: forall s s' x y,
+    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.
+  Proof. intros s s' x y Hx Hy H. apply choose_3' in H. congruence. Qed.
+
+
+  (** Specification of [min_elt] *)
+
+  Lemma min_elt_1: forall s x, min_elt s = Some x -> In x s.
+  Proof.
+   unfold In.
+   induction s as [| l IHl o r IHr]; simpl.
+     intros. discriminate.
+     intros x. destruct (min_elt l); intros.
+       injection H. intros <-. apply IHl. reflexivity.
+       destruct o; simpl.
+         injection H. intros <-. reflexivity.
+         destruct (min_elt r); simpl in *.
+           injection H. intros <-. apply IHr. reflexivity.
+           discriminate.
+  Qed.
+
+  Lemma min_elt_3: forall s, min_elt s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_1.
+      intros [a|a|].
+        apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial.
+          case min_elt; intros; try discriminate. destruct o; discriminate.
+        apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial.
+         intro; discriminate.
+        revert H. clear. simpl. case min_elt; intros; try discriminate.
+         destruct o; discriminate.
+  Qed.
+
+  Lemma min_elt_2: forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x.
+  Proof.
+    unfold In.
+    induction s as [|l IHl o r IHr]; intros x y H H'.
+      discriminate.
+      simpl in H. case_eq (min_elt l).
+        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
+        intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
+        destruct o.
+          injection H. intros <- Hl. clear H.
+          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+          destruct (min_elt r).
+            injection H. intros <-. clear H.
+            destruct y as [z|z|].
+              apply (IHr p z); trivial.
+              elim (Hp _ H').
+              discriminate.
+            discriminate.
+  Qed.
+
+
+  (** Specification of [max_elt] *)
+
+  Lemma max_elt_1: forall s x, max_elt s = Some x -> In x s.
+  Proof.
+   unfold In.
+   induction s as [| l IHl o r IHr]; simpl.
+     intros. discriminate.
+     intros x. destruct (max_elt r); intros.
+       injection H. intros <-. apply IHr. reflexivity.
+       destruct o; simpl.
+         injection H. intros <-. reflexivity.
+         destruct (max_elt l); simpl in *.
+           injection H. intros <-. apply IHl. reflexivity.
+           discriminate.
+  Qed.
+
+  Lemma max_elt_3: forall s, max_elt s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_1.
+      intros [a|a|].
+        apply IHr. revert H. clear. simpl. destruct (max_elt r); trivial.
+         intro; discriminate.
+        apply IHl. revert H. clear. simpl. destruct (max_elt l); trivial.
+          case max_elt; intros; try discriminate. destruct o; discriminate.
+        revert H. clear. simpl. case max_elt; intros; try discriminate.
+         destruct o; discriminate.
+  Qed.
+
+  Lemma max_elt_2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y.
+  Proof.
+    unfold In.
+    induction s as [|l IHl o r IHr]; intros x y H H'.
+      discriminate.
+      simpl in H. case_eq (max_elt r).
+        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
+        intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
+        destruct o.
+          injection H. intros <- Hl. clear H.
+          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+          destruct (max_elt l).
+            injection H. intros <-. clear H.
+            destruct y as [z|z|].
+              elim (Hp _ H').
+              apply (IHl p z); trivial.
+              discriminate.
+            discriminate.
+  Qed.
+
+End PositiveSet.
diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v
index 9a7294119..572f28654 100644
--- a/theories/FSets/FSets.v
+++ b/theories/FSets/FSets.v
@@ -19,4 +19,5 @@ Require Export FSetProperties.
 Require Export FSetEqProperties.
 Require Export FSetWeakList.
 Require Export FSetList.
+Require Export FSetPositive.
 Require Export FSetAVL.
\ No newline at end of file
diff --git a/theories/FSets/vo.itarget b/theories/FSets/vo.itarget
index 67ef9585e..0e7c11fb0 100644
--- a/theories/FSets/vo.itarget
+++ b/theories/FSets/vo.itarget
@@ -8,6 +8,7 @@ FMaps.vo
 FMapWeakList.vo
 FSetCompat.vo
 FSetAVL.vo
+FSetPositive.vo
 FSetBridge.vo
 FSetDecide.vo
 FSetEqProperties.vo
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
new file mode 100644
index 000000000..9bd1b7b89
--- /dev/null
+++ b/theories/MSets/MSetPositive.v
@@ -0,0 +1,1149 @@
+(***********************************************************************)
+(*  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       *)
+(***********************************************************************)
+
+(** Efficient implementation of [FSetInterface.S] for positive keys,
+    inspired from the [FMapPositive] module.
+
+   This module was adapted by Alexandre Ren, Damien Pous, and Thomas
+   Braibant (2010, LIG, CNRS, UMR 5217), from the [FMapPositive]
+   module of Pierre Letouzey and Jean-Christophe Filliâtre, which in
+   turn comes from the [FMap] framework of a work by Xavier Leroy and
+   Sandrine Blazy (used for building certified compilers).
+*)
+
+Require Import Bool BinPos Orders MSetInterface.
+
+Set Implicit Arguments.
+
+Local Open Scope lazy_bool_scope.
+Local Open Scope positive_scope.
+
+Local Unset Elimination Schemes.
+Local Unset Case Analysis Schemes.
+Local Unset Boolean Equality Schemes.
+
+
+(** Even if [positive] can be seen as an ordered type with respect to the
+  usual order (see above), we can also use a lexicographic order over bits
+  (lower bits are considered first). This is more natural when using
+  [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *)
+
+Module PositiveOrderedTypeBits <: UsualOrderedType.
+  Definition t:=positive.
+  Include HasUsualEq <+ UsualIsEq.
+  Definition eqb := Peqb.
+  Definition eqb_eq := Peqb_eq.
+  Include HasEqBool2Dec.
+
+  Fixpoint bits_lt (p q:positive) : Prop :=
+   match p, q with
+   | xH, xI _ => True
+   | xH, _ => False
+   | xO p, xO q => bits_lt p q
+   | xO _, _ => True
+   | xI p, xI q => bits_lt p q
+   | xI _, _ => False
+   end.
+
+  Definition lt:=bits_lt.
+
+  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
+  Proof.
+   induction x; simpl; auto.
+  Qed.
+
+  Lemma bits_lt_trans :
+    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
+  Proof.
+   induction x; destruct y,z; simpl; eauto; intuition.
+  Qed.
+
+  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Proof.
+   intros x x' Hx y y' Hy. rewrite Hx, Hy; intuition.
+  Qed.
+
+  Instance lt_strorder : StrictOrder lt.
+  Proof.
+   split; [ exact bits_lt_antirefl | exact bits_lt_trans ].
+  Qed.
+
+  Fixpoint compare x y :=
+    match x, y with
+      | x~1, y~1 => compare x y
+      | x~1, _ => Gt
+      | x~0, y~0 => compare x y
+      | x~0, _ => Lt
+      | 1, y~1 => Lt
+      | 1, 1 => Eq
+      | 1, y~0 => Gt
+    end.
+
+  Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+  Proof.
+   unfold eq, lt.
+   induction x; destruct y; try constructor; simpl; auto.
+    destruct (IHx y); subst; auto.
+    destruct (IHx y); subst; auto.
+  Qed.
+
+End PositiveOrderedTypeBits.
+
+Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
+
+  Module E:=PositiveOrderedTypeBits.
+
+  Definition elt := positive.
+
+  Inductive tree :=
+    | Leaf : tree
+    | Node : tree -> bool -> tree -> tree.
+
+  Scheme tree_ind := Induction for tree Sort Prop.
+
+  Definition t := tree.
+
+  Definition empty := Leaf.
+
+  Fixpoint is_empty (m : t) : bool :=
+   match m with
+    | Leaf => true
+    | Node l b r => negb b &&& is_empty l &&& is_empty r
+   end.
+
+  Fixpoint mem (i : positive) (m : t) : bool :=
+    match m with
+    | Leaf => false
+    | Node l o r =>
+        match i with
+        | 1 => o
+        | i~0 => mem i l
+        | i~1 => mem i r
+        end
+    end.
+
+  Fixpoint add (i : positive) (m : t) : t :=
+    match m with
+    | Leaf =>
+        match i with
+        | 1 => Node Leaf true Leaf
+        | i~0 => Node (add i Leaf) false Leaf
+        | i~1 => Node Leaf false (add i Leaf)
+        end
+    | Node l o r =>
+        match i with
+        | 1 => Node l true r
+        | i~0 => Node (add i l) o r
+        | i~1 => Node l o (add i r)
+        end
+    end.
+
+  Definition singleton i := add i empty.
+
+  (** helper function to avoid creating empty trees that are not leaves *)
+
+  Definition node l (b: bool) r :=
+    if b then Node l b r else
+     match l,r with
+       | Leaf,Leaf => Leaf
+       | _,_ => Node l false r end.
+
+  Fixpoint remove (i : positive) (m : t) : t :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match i with
+          | 1 => node l false r
+          | i~0 => node (remove i l) o r
+          | i~1 => node l o (remove i r)
+        end
+    end.
+
+  Fixpoint union (m m': t) :=
+    match m with
+      | Leaf => m'
+      | Node l o r =>
+        match m' with
+          | Leaf => m
+          | Node l' o' r' => Node (union l l') (o||o') (union r r')
+        end
+    end.
+
+  Fixpoint inter (m m': t) :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match m' with
+          | Leaf => Leaf
+          | Node l' o' r' => node (inter l l') (o&&o') (inter r r')
+        end
+    end.
+
+  Fixpoint diff (m m': t) :=
+    match m with
+      | Leaf => Leaf
+      | Node l o r =>
+        match m' with
+          | Leaf => m
+          | Node l' o' r' => node (diff l l') (o&&negb o') (diff r r')
+        end
+    end.
+
+  Fixpoint equal (m m': t): bool :=
+    match m with
+      | Leaf => is_empty m'
+      | Node l o r =>
+        match m' with
+          | Leaf => is_empty m
+          | Node l' o' r' => eqb o o' &&& equal l l' &&& equal r r'
+        end
+    end.
+
+  Fixpoint subset (m m': t): bool :=
+    match m with
+      | Leaf => true
+      | Node l o r =>
+        match m' with
+          | Leaf => is_empty m
+          | Node l' o' r' => (negb o ||| o') &&& subset l l' &&& subset r r'
+        end
+    end.
+
+  (** reverses [y] and concatenate it with [x] *)
+
+  Fixpoint rev_append y x :=
+    match y with
+      | 1 => x
+      | y~1 => rev_append y x~1
+      | y~0 => rev_append y x~0
+    end.
+  Infix "@" := rev_append (at level 60).
+  Definition rev x := x@1.
+
+  Section Fold.
+
+    Variables B : Type.
+    Variable f : positive -> B -> B.
+
+    (** the additional argument, [i], records the current path, in
+       reverse order (this should be more efficient: we reverse this argument
+       only at present nodes only, rather than at each node of the tree).
+       we also use this convention in all functions below
+     *)
+
+    Fixpoint xfold (m : t) (v : B) (i : positive) :=
+      match m with
+        | Leaf => v
+        | Node l true r =>
+          xfold r (f (rev i) (xfold l v i~0)) i~1
+        | Node l false r =>
+          xfold r (xfold l v i~0) i~1
+      end.
+    Definition fold m i := xfold m i 1.
+
+  End Fold.
+
+  Section Quantifiers.
+
+    Variable f : positive -> bool.
+
+    Fixpoint xforall (m : t) (i : positive) :=
+      match m with
+        | Leaf => true
+        | Node l o r =>
+          (negb o ||| f (rev i)) &&& xforall r i~1 &&& xforall l i~0
+      end.
+    Definition for_all m := xforall m 1.
+
+    Fixpoint xexists (m : t) (i : positive) :=
+      match m with
+        | Leaf => false
+        | Node l o r => (o &&& f (rev i)) ||| xexists r i~1 ||| xexists l i~0
+      end.
+    Definition exists_ m := xexists m 1.
+
+    Fixpoint xfilter (m : t) (i : positive) :=
+      match m with
+        | Leaf => Leaf
+        | Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
+      end.
+    Definition filter m := xfilter m 1.
+
+    Fixpoint xpartition (m : t) (i : positive) :=
+      match m with
+        | Leaf => (Leaf,Leaf)
+        | Node l o r =>
+          let (lt,lf) := xpartition l i~0 in
+          let (rt,rf) := xpartition r i~1 in
+             if o then
+               let fi := f (rev i) in
+                 (node lt fi rt, node lf (negb fi) rf)
+             else
+                 (node lt false rt, node lf false rf)
+      end.
+    Definition partition m := xpartition m 1.
+
+  End Quantifiers.
+
+  (** uses [a] to accumulate values rather than doing a lot of concatenations *)
+
+  Fixpoint xelements (m : t) (i : positive) (a: list positive) :=
+    match m with
+      | Leaf => a
+      | Node l false r => xelements l i~0 (xelements r i~1 a)
+      | Node l true r => xelements l i~0 (rev i :: xelements r i~1 a)
+    end.
+
+  Definition elements (m : t) := xelements m 1 nil.
+
+  Fixpoint cardinal (m : t) : nat :=
+    match m with
+      | Leaf => O
+      | Node l false r => (cardinal l + cardinal r)%nat
+      | Node l true r => S (cardinal l + cardinal r)
+    end.
+
+  Definition omap (f: elt -> elt) x :=
+    match x with
+      | None => None
+      | Some i => Some (f i)
+    end.
+
+  (** would it be more efficient to use a path like in the above functions ? *)
+
+  Fixpoint choose (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r => if o then Some 1 else
+        match choose l with
+          | None => omap xI (choose r)
+          | Some i => Some i~0
+        end
+    end.
+
+  Fixpoint min_elt (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r =>
+        match min_elt l with
+          | None => if o then Some 1 else omap xI (min_elt r)
+          | Some i => Some i~0
+        end
+    end.
+
+  Fixpoint max_elt (m: t) :=
+    match m with
+      | Leaf => None
+      | Node l o r =>
+        match max_elt r with
+          | None => if o then Some 1 else omap xO (max_elt l)
+          | Some i => Some i~1
+        end
+    end.
+
+  (** lexicographic product, defined using a notation to keep things lazy *)
+
+  Notation lex u v := match u with Eq => v | Lt => Lt | Gt => Gt end.
+
+  Definition compare_bool a b :=
+    match a,b with
+      | false, true => Lt
+      | true, false => Gt
+      | _,_ => Eq
+    end.
+
+  Fixpoint compare (m m': t): comparison :=
+    match m,m' with
+      | Leaf,_ => if is_empty m' then Eq else Lt
+      | _,Leaf => if is_empty m then Eq else Gt
+      | Node l o r,Node l' o' r' =>
+        lex (compare_bool o o') (lex (compare l l') (compare r r'))
+    end.
+
+
+  Definition In i t := mem i t = true.
+  Definition Equal s s' := forall a : elt, In a  s <-> In a  s'.
+  Definition Subset s s' := forall a : elt, In a s -> In a s'.
+  Definition Empty s := forall a : elt, ~ In a s.
+  Definition For_all (P : elt -> Prop) s := forall x, In x s -> P x.
+  Definition Exists (P : elt -> Prop) s := exists x, In x s /\ P x.
+
+  Notation "s  [=]  t" := (Equal s t) (at level 70, no associativity).
+  Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
+
+  Definition eq := Equal.
+  Definition lt m m' := compare m m' = Lt.
+
+  (** Specification of [In] *)
+
+  Instance In_compat : Proper (E.eq==>Logic.eq==>iff) In.
+  Proof.
+   intros s s' Hs x x' Hx. rewrite Hs, Hx; intuition.
+  Qed.
+
+  (** Specification of [eq] *)
+
+  Local Instance eq_equiv : Equivalence eq.
+  Proof. firstorder. Qed.
+
+  (** Specification of [mem] *)
+
+  Lemma mem_spec: forall s x, mem x s = true <-> In x s.
+  Proof. unfold In. intuition. Qed.
+
+  (** Additional lemmas for mem  *)
+
+  Lemma mem_Leaf: forall x, mem x Leaf = false.
+  Proof. destruct x; trivial. Qed.
+
+  (** Specification of [empty] *)
+
+  Lemma empty_spec : Empty empty.
+  Proof. unfold Empty, In. intro. rewrite mem_Leaf. discriminate. Qed.
+
+  (** Specification of node  *)
+
+  Lemma mem_node: forall x l o r, mem x (node l o r) = mem x (Node l o r).
+  Proof.
+    intros x l o r.
+    case o; trivial.
+    destruct l; trivial.
+    destruct r; trivial.
+    symmetry. destruct x.
+      apply mem_Leaf.
+      apply mem_Leaf.
+      reflexivity.
+  Qed.
+  Local Opaque node.
+
+  (** Specification of [is_empty] *)
+
+  Lemma is_empty_spec: forall s, is_empty s = true <-> Empty s.
+  Proof.
+    unfold Empty, In.
+    induction s as [|l IHl o r IHr]; simpl.
+      setoid_rewrite mem_Leaf. firstorder.
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear IHl IHr.
+      destruct o; simpl; split.
+        intuition discriminate.
+        intro H. elim (H 1). reflexivity.
+        intros H [a|a|]; apply H || intro; discriminate.
+        intro H. split. split. reflexivity.
+          intro a. apply (H a~0).
+          intro a. apply (H a~1).
+  Qed.
+
+  (** Specification of [subset] *)
+
+  Lemma subset_Leaf_s: forall s, Leaf [<=] s.
+  Proof. intros s i Hi. apply empty_spec in Hi. elim Hi. Qed.
+
+  Lemma subset_spec: forall s s', subset s s' = true <-> s [<=] s'.
+  Proof.
+    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl.
+      split; intros. apply subset_Leaf_s. reflexivity.
+
+      split; intros. apply subset_Leaf_s. reflexivity.
+
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, 2is_empty_spec.
+      destruct o; simpl.
+        split.
+          intuition discriminate.
+          intro H. elim (@empty_spec 1). apply H. reflexivity.
+        split; intro H.
+          destruct H as [[_ Hl] Hr].
+          intros [i|i|] Hi.
+            elim (Hr i Hi).
+            elim (Hl i Hi).
+            discriminate.
+          split. split. reflexivity.
+          unfold Empty. intros a H1. apply (@empty_spec (a~0)), H. assumption.
+          unfold Empty. intros a H1. apply (@empty_spec (a~1)), H. assumption.
+
+      rewrite <- 2andb_lazy_alt, 2andb_true_iff, IHl, IHr. clear.
+      destruct o; simpl.
+       split; intro H.
+         destruct H as [[Ho' Hl] Hr]. rewrite Ho'.
+          intros i Hi. destruct i.
+            apply (Hr i). assumption.
+            apply (Hl i). assumption.
+            assumption.
+         split. split.
+          destruct o'; trivial.
+          specialize (H 1). unfold In in H. simpl in H. apply H. reflexivity.
+          intros i Hi. apply (H i~0). apply Hi.
+          intros i Hi. apply (H i~1). apply Hi.
+       split; intros.
+         intros i Hi. destruct i; destruct H as [[H Hl] Hr].
+           apply (Hr i). assumption.
+           apply (Hl i). assumption.
+            discriminate Hi.
+         split. split. reflexivity.
+           intros i Hi. apply (H i~0). apply Hi.
+           intros i Hi. apply (H i~1). apply Hi.
+  Qed.
+
+  (** Specification of [equal] (via subset) *)
+
+  Lemma equal_subset: forall s s', equal s s' = subset s s' && subset s' s.
+  Proof.
+    induction s as [|l IHl o r IHr]; intros [|l' o' r']; simpl; trivial.
+      destruct o. reflexivity. rewrite andb_comm. reflexivity.
+      rewrite <- 6andb_lazy_alt. rewrite eq_iff_eq_true.
+       rewrite 7andb_true_iff, eqb_true_iff.
+      rewrite IHl, IHr, 2andb_true_iff. clear IHl IHr. intuition subst.
+       destruct o'; reflexivity.
+       destruct o'; reflexivity.
+       destruct o; auto. destruct o'; trivial.
+  Qed.
+
+  Lemma equal_spec: forall s s', equal s s' = true <-> Equal s s'.
+  Proof.
+    intros. rewrite equal_subset. rewrite andb_true_iff.
+    rewrite 2subset_spec. unfold Equal, Subset. firstorder.
+  Qed.
+
+  Lemma eq_dec : forall s s', { eq s s' } + { ~ eq s s' }.
+  Proof.
+    unfold eq.
+    intros. case_eq (equal s s'); intro H.
+     left. apply equal_spec, H.
+     right. rewrite <- equal_spec. congruence.
+  Defined.
+
+  (** (Specified) definition of [compare] *)
+
+  Lemma lex_Opp: forall u v u' v', u = CompOpp u' -> v = CompOpp v' ->
+    lex u v = CompOpp (lex u' v').
+  Proof. intros ? ? u' ? -> ->. case u'; reflexivity. Qed.
+
+  Lemma compare_bool_inv: forall b b',
+    compare_bool b b' = CompOpp (compare_bool b' b).
+  Proof. intros [|] [|]; reflexivity. Qed.
+
+  Lemma compare_inv: forall s s', compare s s' = CompOpp (compare s' s).
+  Proof.
+    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r']; trivial.
+    unfold compare. case is_empty; reflexivity.
+    unfold compare. case is_empty; reflexivity.
+    simpl. rewrite compare_bool_inv.
+     case compare_bool; simpl; trivial; apply lex_Opp; auto.
+  Qed.
+
+  Lemma lex_Eq: forall u v, lex u v = Eq <-> u=Eq /\ v=Eq.
+  Proof. intros u v; destruct u; intuition discriminate. Qed.
+
+  Lemma compare_bool_Eq: forall b1 b2,
+    compare_bool b1 b2 = Eq <-> eqb b1 b2 = true.
+  Proof. intros [|] [|]; intuition discriminate. Qed.
+
+  Lemma compare_equal: forall s s', compare s s' = Eq <-> equal s s' = true.
+  Proof.
+    induction s as [|l IHl o r IHr]; destruct s' as [|l' o' r'].
+     simpl. tauto.
+     unfold compare, equal. case is_empty; intuition discriminate.
+     unfold compare, equal. case is_empty; intuition discriminate.
+     simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff.
+     rewrite <- IHl, <- IHr, <- compare_bool_Eq. clear IHl IHr.
+     rewrite and_assoc. rewrite <- 2lex_Eq. reflexivity.
+  Qed.
+
+
+  Lemma compare_gt: forall s s', compare s s' = Gt -> lt s' s.
+  Proof.
+    unfold lt. intros s s'. rewrite compare_inv.
+     case compare; trivial; intros; discriminate.
+  Qed.
+
+  Lemma compare_eq: forall s s', compare s s' = Eq -> eq s s'.
+  Proof.
+    unfold eq. intros s s'. rewrite compare_equal, equal_spec. trivial.
+  Qed.
+
+  Lemma compare_spec : forall s s' : t, CompSpec eq lt s s' (compare s s').
+  Proof.
+    intros. case_eq (compare s s'); intro H; constructor.
+    apply compare_eq, H.
+    assumption.
+    apply compare_gt, H.
+  Qed.
+
+  Section lt_spec.
+
+  Inductive ct: comparison -> comparison -> comparison -> Prop :=
+  | ct_xxx: forall x, ct x  x  x
+  | ct_xex: forall x, ct x  Eq x
+  | ct_exx: forall x, ct Eq x  x
+  | ct_glx: forall x, ct Gt Lt x
+  | ct_lgx: forall x, ct Lt Gt x.
+
+  Lemma ct_cxe: forall x, ct (CompOpp x) x Eq.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xce: forall x, ct x (CompOpp x) Eq.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_lxl: forall x, ct Lt x Lt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_gxg: forall x, ct Gt x Gt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xll: forall x, ct x Lt Lt.
+  Proof. destruct x; constructor. Qed.
+
+  Lemma ct_xgg: forall x, ct x Gt Gt.
+  Proof. destruct x; constructor. Qed.
+
+  Local Hint Constructors ct: ct.
+  Local Hint Resolve ct_cxe ct_xce ct_lxl ct_xll ct_gxg ct_xgg: ct.
+  Ltac ct := trivial with ct.
+
+  Lemma ct_lex: forall u v w u' v' w',
+    ct u v w -> ct u' v' w' -> ct (lex u u') (lex v v') (lex w w').
+  Proof.
+    intros u v w u' v' w' H H'.
+    inversion_clear H; inversion_clear H'; ct; destruct w; ct; destruct w'; ct.
+  Qed.
+
+  Lemma ct_compare_bool:
+    forall a b c, ct (compare_bool a b) (compare_bool b c) (compare_bool a c).
+  Proof.
+    intros [|] [|] [|]; constructor.
+  Qed.
+
+  Lemma compare_x_Leaf: forall s,
+    compare s Leaf = if is_empty s then Eq else Gt.
+  Proof.
+    intros. rewrite compare_inv. simpl. case (is_empty s); reflexivity.
+  Qed.
+
+  Lemma compare_empty_x: forall a, is_empty a = true ->
+    forall b, compare a b = if is_empty b then Eq else Lt.
+  Proof.
+    induction a as [|l IHl o r IHr]; trivial.
+    destruct o. intro; discriminate.
+    simpl is_empty. rewrite <- andb_lazy_alt, andb_true_iff.
+    intros [Hl Hr].
+    destruct b as [|l' [|] r']; simpl compare; trivial.
+     rewrite Hl, Hr. trivial.
+     rewrite (IHl Hl), (IHr Hr). simpl.
+     case (is_empty l'); case (is_empty r'); trivial.
+  Qed.
+
+  Lemma compare_x_empty: forall a, is_empty a = true ->
+    forall b, compare b a = if is_empty b then Eq else Gt.
+  Proof.
+    setoid_rewrite <- compare_x_Leaf.
+    intros. rewrite 2(compare_inv b), (compare_empty_x _ H). reflexivity.
+  Qed.
+
+  Lemma ct_compare:
+    forall a b c, ct (compare a b) (compare b c) (compare a c).
+  Proof.
+    induction a as [|l IHl o r IHr]; intros s' s''.
+     destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r'']; ct.
+      rewrite compare_inv. ct.
+      unfold compare at 1. case_eq (is_empty (Node l' o' r')); intro H'.
+       rewrite (compare_empty_x _ H'). ct.
+       unfold compare at 2. case_eq (is_empty (Node l'' o'' r'')); intro H''.
+        rewrite (compare_x_empty _ H''), H'. ct.
+        ct.
+
+     destruct s' as [|l' o' r']; destruct s'' as [|l'' o'' r''].
+      ct.
+      unfold compare at 2. rewrite compare_x_Leaf.
+      case_eq (is_empty (Node l o r)); intro H.
+       rewrite (compare_empty_x _ H). ct.
+       case_eq (is_empty (Node l'' o'' r'')); intro H''.
+        rewrite (compare_x_empty _ H''), H. ct.
+        ct.
+
+      rewrite 2 compare_x_Leaf.
+      case_eq (is_empty (Node l o r)); intro H.
+       rewrite compare_inv, (compare_x_empty _ H). ct.
+       case_eq (is_empty (Node l' o' r')); intro H'.
+        rewrite (compare_x_empty _ H'), H. ct.
+        ct.
+
+      simpl compare. apply ct_lex. apply ct_compare_bool.
+       apply ct_lex; trivial.
+  Qed.
+
+  End lt_spec.
+
+  Instance lt_strorder : StrictOrder lt.
+  Proof.
+   unfold lt. split.
+   intros x H.
+   assert (compare x x = Eq).
+    apply compare_equal, equal_spec. reflexivity.
+   congruence.
+   intros a b c. assert (H := ct_compare a b c).
+    inversion_clear H; trivial; intros; discriminate.
+  Qed.
+
+  Local Instance compare_compat_1 : Proper (eq==>Logic.eq==>Logic.eq) compare.
+  Proof.
+   intros x x' Hx y y' Hy. subst y'.
+   unfold eq in *. rewrite <- equal_spec, <- compare_equal in *.
+   assert (C:=ct_compare x x' y). rewrite Hx in C. inversion C; auto.
+  Qed.
+
+  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
+  Proof.
+   intros x x' Hx y y' Hy. rewrite Hx.
+   rewrite compare_inv, Hy, <- compare_inv. reflexivity.
+  Qed.
+
+  Local Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Proof.
+   intros x x' Hx y y' Hy. unfold lt. rewrite Hx, Hy. intuition.
+  Qed.
+
+  (** Specification of [add] *)
+
+  Lemma add_spec: forall s x y, In y (add x s) <-> y=x \/ In y s.
+  Proof.
+    unfold In. intros s x y; revert x y s.
+    induction x; intros [y|y|] [|l o r]; simpl mem;
+    try (rewrite IHx; clear IHx); rewrite ?mem_Leaf; intuition congruence.
+  Qed.
+
+  (** Specification of [remove] *)
+
+  Lemma remove_spec: forall s x y, In y (remove x s) <-> In y s /\ y<>x.
+  Proof.
+    unfold In. intros s x y; revert x y s.
+    induction x; intros [y|y|] [|l o r]; simpl remove; rewrite ?mem_node;
+     simpl mem; try (rewrite IHx; clear IHx); rewrite ?mem_Leaf;
+     intuition congruence.
+  Qed.
+
+  (** Specification of [singleton] *)
+
+  Lemma singleton_spec : forall x y, In y (singleton x) <-> y=x.
+  Proof.
+    unfold singleton. intros x y. rewrite add_spec. intuition.
+    unfold In in *. rewrite mem_Leaf in *. discriminate.
+  Qed.
+
+  (** Specification of [union] *)
+
+  Lemma union_spec: forall s s' x, In x (union s s') <-> In x s \/ In x s'.
+  Proof.
+    unfold In. intros s s' x; revert x s s'.
+    induction x; destruct s; destruct s'; simpl union; simpl mem;
+      try (rewrite IHx; clear IHx); try intuition congruence.
+      apply orb_true_iff.
+  Qed.
+
+  (** Specification of [inter] *)
+
+  Lemma inter_spec: forall s s' x, In x (inter s s') <-> In x s /\ In x s'.
+  Proof.
+    unfold In. intros s s' x; revert x s s'.
+    induction x; destruct s; destruct s'; simpl inter; rewrite ?mem_node;
+     simpl mem; try (rewrite IHx; clear IHx); try intuition congruence.
+     apply andb_true_iff.
+  Qed.
+
+  (** Specification of [diff] *)
+
+  Lemma diff_spec: forall s s' x, In x (diff s s') <-> In x s /\ ~ In x s'.
+  Proof.
+    unfold In. intros s s' x; revert x s s'.
+    induction x; destruct s; destruct s' as [|l' o' r']; simpl diff;
+     rewrite ?mem_node; simpl mem;
+      try (rewrite IHx; clear IHx); try intuition congruence.
+      rewrite andb_true_iff. destruct o'; intuition discriminate.
+  Qed.
+
+  (** Specification of [fold] *)
+
+  Lemma fold_spec: forall s (A : Type) (i : A) (f : elt -> A -> A),
+      fold f s i = fold_left (fun a e => f e a) (elements s) i.
+  Proof.
+    unfold fold, elements. intros s A i f. revert s i.
+    set (f' := fun a e => f e a).
+    assert (H: forall s i j acc,
+      fold_left f' acc (xfold f s i j) =
+      fold_left f' (xelements s j acc) i).
+
+    induction s as [|l IHl o r IHr]; intros; trivial.
+      destruct o; simpl xelements; simpl xfold.
+        rewrite IHr, <- IHl. reflexivity.
+        rewrite IHr. apply IHl.
+
+    intros. exact (H s i 1 nil).
+  Qed.
+
+  (** Specification of [cardinal] *)
+
+  Lemma cardinal_spec: forall s, cardinal s = length (elements s).
+  Proof.
+    unfold elements.
+    assert (H: forall s j acc,
+                (cardinal s + length acc)%nat = length (xelements s j acc)).
+
+    induction s as [|l IHl b r IHr]; intros j acc; simpl; trivial. destruct b.
+      rewrite <- IHl. simpl. rewrite <- IHr.
+       rewrite <- plus_n_Sm, Plus.plus_assoc. reflexivity.
+      rewrite <- IHl, <- IHr. rewrite Plus.plus_assoc. reflexivity.
+
+    intros. rewrite <- H. simpl. rewrite Plus.plus_comm. reflexivity.
+  Qed.
+
+  (** Specification of [filter] *)
+
+  Lemma xfilter_spec: forall f s x i,
+    In x (xfilter f s i) <-> In x s /\ f (i@x) = true.
+  Proof.
+    intro f. unfold In.
+    induction s as [|l IHl o r IHr]; intros x i; simpl xfilter.
+     rewrite mem_Leaf. intuition discriminate.
+     rewrite mem_node. destruct x; simpl.
+       rewrite IHr. reflexivity.
+       rewrite IHl. reflexivity.
+       rewrite <- andb_lazy_alt. apply andb_true_iff.
+  Qed.
+
+  Lemma filter_spec: forall s x f, compat_bool E.eq f ->
+    (In x (filter f s) <-> In x s /\ f x = true).
+  Proof. intros. apply xfilter_spec. Qed.
+
+  (** Specification of [for_all] *)
+
+  Lemma xforall_spec: forall f s i,
+    xforall f s i = true <-> For_all (fun x => f (i@x) = true) s.
+  Proof.
+    unfold For_all, In. intro f.
+    induction s as [|l IHl o r IHr]; intros i; simpl.
+     setoid_rewrite mem_Leaf. intuition discriminate.
+     rewrite <- 2andb_lazy_alt, <- orb_lazy_alt, 2 andb_true_iff.
+     rewrite IHl, IHr. clear IHl IHr.
+      split.
+       intros [[Hi Hr] Hl] x. destruct x; simpl; intro H.
+        apply Hr, H.
+        apply Hl, H.
+        rewrite H in Hi. assumption.
+       intro H; intuition.
+        specialize (H 1). destruct o. apply H. reflexivity. reflexivity.
+        apply H. assumption.
+        apply H. assumption.
+  Qed.
+
+  Lemma for_all_spec: forall s f, compat_bool E.eq f ->
+    (for_all f s = true <-> For_all (fun x => f x = true) s).
+  Proof. intros. apply xforall_spec. Qed.
+
+  (** Specification of [exists] *)
+
+  Lemma xexists_spec: forall f s i,
+    xexists f s i = true <-> Exists (fun x => f (i@x) = true) s.
+  Proof.
+    unfold Exists, In. intro f.
+    induction s as [|l IHl o r IHr]; intros i; simpl.
+     setoid_rewrite mem_Leaf. firstorder.
+     rewrite <- 2orb_lazy_alt, 2orb_true_iff, <- andb_lazy_alt, andb_true_iff.
+     rewrite IHl, IHr. clear IHl IHr.
+      split.
+       intros [[Hi|[x Hr]]|[x Hl]].
+        exists 1. exact Hi.
+        exists x~1. exact Hr.
+        exists x~0. exact Hl.
+       intros [[x|x|] H]; eauto.
+  Qed.
+
+  Lemma exists_spec : forall s f, compat_bool E.eq f ->
+    (exists_ f s = true <-> Exists (fun x => f x = true) s).
+  Proof. intros. apply xexists_spec. Qed.
+
+
+  (** Specification of [partition] *)
+
+  Lemma partition_filter : forall s f,
+    partition f s = (filter f s, filter (fun x => negb (f x)) s).
+  Proof.
+    unfold partition, filter. intros s f. generalize 1 as j.
+    induction s as [|l IHl o r IHr]; intro j.
+      reflexivity.
+      destruct o; simpl; rewrite IHl, IHr; reflexivity.
+  Qed.
+
+  Lemma partition_spec1 : forall s f, compat_bool E.eq f ->
+      Equal (fst (partition f s)) (filter f s).
+  Proof. intros. rewrite partition_filter. reflexivity. Qed.
+
+  Lemma partition_spec2 : forall s f, compat_bool E.eq f ->
+      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
+  Proof. intros. rewrite partition_filter. reflexivity. Qed.
+
+
+  (** Specification of [elements] *)
+
+  Notation InL := (InA E.eq).
+
+  Lemma xelements_spec: forall s j acc y,
+    InL y (xelements s j acc)
+    <->
+    InL y acc \/ exists x, y=(j@x) /\ mem x s = true.
+  Proof.
+    induction s as [|l IHl o r IHr]; simpl.
+      intros. split; intro H.
+        left. assumption.
+        destruct H as [H|[x [Hx Hx']]]. assumption. elim (empty_spec Hx').
+
+      intros j acc y. case o.
+        rewrite IHl. rewrite InA_cons. rewrite IHr. clear IHl IHr. split.
+          intros [[H|[H|[x [-> H]]]]|[x [-> H]]]; eauto.
+            right. exists x~1. auto.
+            right. exists x~0. auto.
+          intros [H|[x [-> H]]].
+            eauto.
+            destruct x.
+              left. right. right. exists x; auto.
+              right. exists x; auto.
+              left. left. reflexivity.
+
+        rewrite IHl, IHr. clear IHl IHr. split.
+          intros [[H|[x [-> H]]]|[x [-> H]]].
+            eauto.
+            right. exists x~1. auto.
+            right. exists x~0. auto.
+          intros [H|[x [-> H]]].
+            eauto.
+            destruct x.
+              left. right.  exists x; auto.
+              right. exists x; auto.
+              discriminate.
+  Qed.
+
+  Lemma elements_spec1: forall s x, InL x (elements s) <-> In x s.
+  Proof.
+   unfold elements. intros. rewrite xelements_spec.
+   split; [ intros [A|(y & B & C)] | intros IN ].
+   inversion A. simpl in *. congruence.
+   right. exists x. auto.
+  Qed.
+
+  Lemma lt_rev_append: forall j x y, E.lt x y -> E.lt (j@x) (j@y).
+  Proof. induction j; intros; simpl; auto. Qed.
+
+  Lemma elements_spec2: forall s, sort E.lt (elements s).
+  Proof.
+    unfold elements.
+    assert (H: forall s j acc,
+      sort E.lt acc ->
+      (forall x y, In x s ->  InL y acc -> E.lt (j@x) y) ->
+      sort E.lt (xelements s j acc)).
+
+    induction s as [|l IHl o r IHr]; simpl; trivial.
+    intros j acc Hacc Hsacc. destruct o.
+      apply IHl. constructor.
+       apply IHr. apply Hacc.
+       intros x y Hx Hy. apply Hsacc; assumption.
+       case_eq (xelements r j~1 acc). constructor.
+       intros z q H. constructor.
+       assert (H': InL z (xelements r j~1 acc)).
+        rewrite H. constructor. reflexivity.
+       clear H q. rewrite xelements_spec in H'. destruct H' as [Hy|[x [-> Hx]]].
+         apply (Hsacc 1 z); trivial. reflexivity.
+         simpl. apply lt_rev_append. exact I.
+       intros x y Hx Hy. inversion_clear Hy.
+         rewrite H. simpl. apply lt_rev_append. exact I.
+         rewrite xelements_spec in H. destruct H as [Hy|[z [-> Hy]]].
+           apply Hsacc; assumption.
+           simpl. apply lt_rev_append. exact I.
+
+      apply IHl. apply IHr. apply Hacc.
+       intros x y Hx Hy. apply Hsacc; assumption.
+       intros x y Hx Hy. rewrite xelements_spec in Hy.
+        destruct Hy as [Hy|[z [-> Hy]]].
+         apply Hsacc; assumption.
+         simpl. apply lt_rev_append. exact I.
+
+    intros. apply H. constructor.
+      intros x y _ H'. inversion H'.
+  Qed.
+
+  Lemma elements_spec2w: forall s, NoDupA E.eq (elements s).
+  Proof.
+    intro. apply SortA_NoDupA with E.lt; auto with *.
+    apply E.eq_equiv.
+    apply elements_spec2.
+  Qed.
+
+
+  (** Specification of [choose] *)
+
+  Lemma choose_spec1: forall s x, choose s = Some x -> In x s.
+  Proof.
+    induction s as [| l IHl o r IHr]; simpl.
+      intros. discriminate.
+      destruct o.
+        intros x H. injection H; intros; subst. reflexivity.
+        revert IHl. case choose.
+          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+           reflexivity.
+          intros _ x. revert IHr. case choose.
+            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            reflexivity.
+            intros. discriminate.
+  Qed.
+
+  Lemma choose_spec2: forall s, choose s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_spec.
+      destruct o.
+        discriminate.
+        simpl in H. destruct (choose l).
+          discriminate.
+          destruct (choose r).
+            discriminate.
+            intros [a|a|].
+              apply IHr. reflexivity.
+              apply IHl. reflexivity.
+              discriminate.
+  Qed.
+
+  Lemma choose_empty: forall s, is_empty s = true -> choose s = None.
+  Proof.
+    intros s Hs. case_eq (choose s); trivial.
+    intros p Hp. apply choose_spec1 in Hp. apply is_empty_spec in Hs.
+     elim (Hs _ Hp).
+  Qed.
+
+  Lemma choose_spec3': forall s s', Equal s s' -> choose s = choose s'.
+  Proof.
+    setoid_rewrite <- equal_spec.
+    induction s as [|l IHl o r IHr].
+      intros. symmetry. apply choose_empty. assumption.
+
+      destruct s' as [|l' o' r'].
+        generalize (Node l o r) as s. simpl. intros. apply choose_empty.
+        rewrite equal_spec in H. symmetry in H. rewrite <- equal_spec in H.
+        assumption.
+
+        simpl. rewrite <- 2andb_lazy_alt, 2andb_true_iff, eqb_true_iff.
+        intros [[<- Hl] Hr]. rewrite (IHl _ Hl), (IHr _ Hr). reflexivity.
+  Qed.
+
+  Lemma choose_spec3: forall s s' x y,
+    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.
+  Proof. intros s s' x y Hx Hy H. apply choose_spec3' in H. congruence. Qed.
+
+
+  (** Specification of [min_elt] *)
+
+  Lemma min_elt_spec1: forall s x, min_elt s = Some x -> In x s.
+  Proof.
+   unfold In.
+   induction s as [| l IHl o r IHr]; simpl.
+     intros. discriminate.
+     intros x. destruct (min_elt l); intros.
+       injection H. intros <-. apply IHl. reflexivity.
+       destruct o; simpl.
+         injection H. intros <-. reflexivity.
+         destruct (min_elt r); simpl in *.
+           injection H. intros <-. apply IHr. reflexivity.
+           discriminate.
+  Qed.
+
+  Lemma min_elt_spec3: forall s, min_elt s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_spec.
+      intros [a|a|].
+        apply IHr. revert H. clear. simpl. destruct (min_elt r); trivial.
+          case min_elt; intros; try discriminate. destruct o; discriminate.
+        apply IHl. revert H. clear. simpl. destruct (min_elt l); trivial.
+         intro; discriminate.
+        revert H. clear. simpl. case min_elt; intros; try discriminate.
+         destruct o; discriminate.
+  Qed.
+
+  Lemma min_elt_spec2: forall s x y, min_elt s = Some x -> In y s -> ~ E.lt y x.
+  Proof.
+    unfold In.
+    induction s as [|l IHl o r IHr]; intros x y H H'.
+      discriminate.
+      simpl in H. case_eq (min_elt l).
+        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
+        intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp.
+        destruct o.
+          injection H. intros <- Hl. clear H.
+          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+          destruct (min_elt r).
+            injection H. intros <-. clear H.
+            destruct y as [z|z|].
+              apply (IHr p z); trivial.
+              elim (Hp _ H').
+              discriminate.
+            discriminate.
+  Qed.
+
+
+  (** Specification of [max_elt] *)
+
+  Lemma max_elt_spec1: forall s x, max_elt s = Some x -> In x s.
+  Proof.
+   unfold In.
+   induction s as [| l IHl o r IHr]; simpl.
+     intros. discriminate.
+     intros x. destruct (max_elt r); intros.
+       injection H. intros <-. apply IHr. reflexivity.
+       destruct o; simpl.
+         injection H. intros <-. reflexivity.
+         destruct (max_elt l); simpl in *.
+           injection H. intros <-. apply IHl. reflexivity.
+           discriminate.
+  Qed.
+
+  Lemma max_elt_spec3: forall s, max_elt s = None -> Empty s.
+  Proof.
+    unfold Empty, In. intros s H.
+    induction s as [|l IHl o r IHr].
+      intro. apply empty_spec.
+      intros [a|a|].
+        apply IHr. revert H. clear. simpl. destruct (max_elt r); trivial.
+         intro; discriminate.
+        apply IHl. revert H. clear. simpl. destruct (max_elt l); trivial.
+          case max_elt; intros; try discriminate. destruct o; discriminate.
+        revert H. clear. simpl. case max_elt; intros; try discriminate.
+         destruct o; discriminate.
+  Qed.
+
+  Lemma max_elt_spec2: forall s x y, max_elt s = Some x -> In y s -> ~ E.lt x y.
+  Proof.
+    unfold In.
+    induction s as [|l IHl o r IHr]; intros x y H H'.
+      discriminate.
+      simpl in H. case_eq (max_elt r).
+        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
+        intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp.
+        destruct o.
+          injection H. intros <- Hl. clear H.
+          destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
+
+          destruct (max_elt l).
+            injection H. intros <-. clear H.
+            destruct y as [z|z|].
+              elim (Hp _ H').
+              apply (IHl p z); trivial.
+              discriminate.
+            discriminate.
+  Qed.
+
+End PositiveSet.
diff --git a/theories/MSets/MSets.v b/theories/MSets/MSets.v
index a4b9efc3b..f179bcd1d 100644
--- a/theories/MSets/MSets.v
+++ b/theories/MSets/MSets.v
@@ -17,4 +17,5 @@ Require Export MSetProperties.
 Require Export MSetEqProperties.
 Require Export MSetWeakList.
 Require Export MSetList.
+Require Export MSetPositive.
 Require Export MSetAVL.
\ No newline at end of file
diff --git a/theories/MSets/vo.itarget b/theories/MSets/vo.itarget
index 970d73d1f..14429b81d 100644
--- a/theories/MSets/vo.itarget
+++ b/theories/MSets/vo.itarget
@@ -8,3 +8,4 @@ MSetProperties.vo
 MSets.vo
 MSetToFiniteSet.vo
 MSetWeakList.vo
+MSetPositive.vo
\ No newline at end of file
diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v
index 600eabf11..496fca074 100644
--- a/theories/Structures/OrderedTypeEx.v
+++ b/theories/Structures/OrderedTypeEx.v
@@ -239,3 +239,93 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType.
 
 End PairOrderedType.
 
+
+(** Even if [positive] can be seen as an ordered type with respect to the
+  usual order (see above), we can also use a lexicographic order over bits
+  (lower bits are considered first). This is more natural when using
+  [positive] as indexes for sets or maps (see FSetPositive and FMapPositive. *)
+
+Module PositiveOrderedTypeBits <: UsualOrderedType.
+  Definition t:=positive.
+  Definition eq:=@eq positive.
+  Definition eq_refl := @refl_equal t.
+  Definition eq_sym := @sym_eq t.
+  Definition eq_trans := @trans_eq t.
+
+  Fixpoint bits_lt (p q:positive) : Prop :=
+   match p, q with
+   | xH, xI _ => True
+   | xH, _ => False
+   | xO p, xO q => bits_lt p q
+   | xO _, _ => True
+   | xI p, xI q => bits_lt p q
+   | xI _, _ => False
+   end.
+
+  Definition lt:=bits_lt.
+
+  Lemma bits_lt_trans :
+    forall x y z : positive, bits_lt x y -> bits_lt y z -> bits_lt x z.
+  Proof.
+  induction x.
+  induction y; destruct z; simpl; eauto; intuition.
+  induction y; destruct z; simpl; eauto; intuition.
+  induction y; destruct z; simpl; eauto; intuition.
+  Qed.
+
+  Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
+  Proof.
+  exact bits_lt_trans.
+  Qed.
+
+  Lemma bits_lt_antirefl : forall x : positive, ~ bits_lt x x.
+  Proof.
+  induction x; simpl; auto.
+  Qed.
+
+  Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
+  Proof.
+  intros; intro.
+  rewrite <- H0 in H; clear H0 y.
+  unfold lt in H.
+  exact (bits_lt_antirefl x H).
+  Qed.
+
+  Definition compare : forall x y : t, Compare lt eq x y.
+  Proof.
+  induction x; destruct y.
+  (* I I *)
+  destruct (IHx y).
+  apply LT; auto.
+  apply EQ; rewrite e; red; auto.
+  apply GT; auto.
+  (* I O *)
+  apply GT; simpl; auto.
+  (* I H *)
+  apply GT; simpl; auto.
+  (* O I *)
+  apply LT; simpl; auto.
+  (* O O *)
+  destruct (IHx y).
+  apply LT; auto.
+  apply EQ; rewrite e; red; auto.
+  apply GT; auto.
+  (* O H *)
+  apply LT; simpl; auto.
+  (* H I *)
+  apply LT; simpl; auto.
+  (* H O *)
+  apply GT; simpl; auto.
+  (* H H *)
+  apply EQ; red; auto.
+  Qed.
+
+  Lemma eq_dec (x y: positive): {x = y} + {x <> y}.
+  Proof.
+  intros. case_eq ((x ?= y) Eq); intros.
+  left. apply Pcompare_Eq_eq; auto.
+  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  right. red. intro. subst y. rewrite (Pcompare_refl x) in H. discriminate.
+  Qed.
+
+End PositiveOrderedTypeBits.