Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Finite set library

Set interfaces, inspired by the one of Ocaml. When compared with Ocaml, the main differences are:

the lack of iter function, useless since Coq is purely functional
the use of option types instead of Not_found exceptions
the use of nat instead of int for the cardinal function

Several variants of the set interfaces are available:

WSetsOn : functorial signature for weak sets
WSets : self-contained version of WSets
SetsOn : functorial signature for ordered sets
Sets : self-contained version of Sets
WRawSets : a signature for weak sets that may be ill-formed
RawSets : same for ordered sets

If unsure, S = Sets is probably what you're looking for: most other signatures are subsets of it, while Sets can be obtained from RawSets via the use of a subset type (see (W)Raw2Sets below).

Require Export Bool SetoidList RelationClasses Morphisms
 RelationPairs Equalities Orders OrdersFacts.
Set Implicit Arguments.
Unset Strict Implicit.

Module Type TypElt.
 Parameters t elt : Type.
End TypElt.

Module Type HasWOps (Import T:TypElt).

  Parameter empty : t.

The empty set.

  Parameter is_empty : t -> bool.

Test whether a set is empty or not.

  Parameter mem : elt -> t -> bool.

mem x s tests whether x belongs to the set s.

  Parameter add : elt -> t -> t.

add x s returns a set containing all elements of s, plus x. If x was already in s, s is returned unchanged.

  Parameter singleton : elt -> t.

singleton x returns the one-element set containing only x.

  Parameter remove : elt -> t -> t.

remove x s returns a set containing all elements of s, except x. If x was not in s, s is returned unchanged.

  Parameter union : t -> t -> t.

Set union.

  Parameter inter : t -> t -> t.

Set intersection.

  Parameter diff : t -> t -> t.

Set difference.

  Parameter equal : t -> t -> bool.

equal s1 s2 tests whether the sets s1 and s2 are equal, that is, contain equal elements.

  Parameter subset : t -> t -> bool.

subset s1 s2 tests whether the set s1 is a subset of the set s2.

  Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.

fold f s a computes (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s. The order in which elements of s are presented to f is unspecified.

  Parameter for_all : (elt -> bool) -> t -> bool.

for_all p s checks if all elements of the set satisfy the predicate p.

  Parameter exists_ : (elt -> bool) -> t -> bool.

∃ p s checks if at least one element of the set satisfies the predicate p.

  Parameter filter : (elt -> bool) -> t -> t.

filter p s returns the set of all elements in s that satisfy predicate p.

  Parameter partition : (elt -> bool) -> t -> t * t.

partition p s returns a pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate p, and s2 is the set of all the elements of s that do not satisfy p.

  Parameter cardinal : t -> nat.

Return the number of elements of a set.

  Parameter elements : t -> list elt.

Return the list of all elements of the given set, in any order.

  Parameter choose : t -> option elt.

Return one element of the given set, or None if the set is empty. Which element is chosen is unspecified. Equal sets could return different elements.

End HasWOps.

Module Type WOps (E : DecidableType).
  Definition elt := E.t.
  Parameter t : Type.

the abstract type of sets

  Include HasWOps.
End WOps.

Functorial signature for weak sets

Weak sets are sets without ordering on base elements, only a decidable equality.

Module Type WSetsOn (E : DecidableType).

First, we ask for all the functions

  Include WOps E.

Logical predicates

  Parameter In : elt -> t -> Prop.
  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.

  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 : t -> t -> Prop := Equal.
  Include IsEq.

eq is obviously an equivalence, for subtyping only

  Include HasEqDec.

Specifications of set operators

  Section Spec.
  Variable s s': t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Parameter mem_spec : mem x s = true <-> In x s.
  Parameter equal_spec : equal s s' = true <-> s[=]s'.
  Parameter subset_spec : subset s s' = true <-> s[<=]s'.
  Parameter empty_spec : Empty empty.
  Parameter is_empty_spec : is_empty s = true <-> Empty s.
  Parameter add_spec : In y (add x s) <-> E.eq y x \/ In y s.
  Parameter remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.
  Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
  Parameter union_spec : In x (union s s') <-> In x s \/ In x s'.
  Parameter inter_spec : In x (inter s s') <-> In x s /\ In x s'.
  Parameter diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.
  Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (flip f) (elements s) i.
  Parameter cardinal_spec : cardinal s = length (elements s).
  Parameter filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).
  Parameter for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).
  Parameter exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).
  Parameter partition_spec1 : compatb f ->
    fst (partition f s) [=] filter f s.
  Parameter partition_spec2 : compatb f ->
    snd (partition f s) [=] filter (fun x => negb (f x)) s.
  Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.

When compared with ordered sets, here comes the only property that is really weaker:

  Parameter elements_spec2w : NoDupA E.eq (elements s).
  Parameter choose_spec1 : choose s = Some x -> In x s.
  Parameter choose_spec2 : choose s = None -> Empty s.

  End Spec.

End WSetsOn.

Static signature for weak sets

Similar to the functorial signature WSetsOn, except that the module E of base elements is incorporated in the signature.

Module Type WSets.
  Declare Module E : DecidableType.
  Include WSetsOn E.
End WSets.

Functorial signature for sets on ordered elements

Based on WSetsOn, plus ordering on sets and min_elt and max_elt and some stronger specifications for other functions.

Module Type HasOrdOps (Import T:TypElt).

  Parameter compare : t -> t -> comparison.

Total ordering between sets. Can be used as the ordering function for doing sets of sets.

  Parameter min_elt : t -> option elt.

Return the smallest element of the given set (with respect to the E.compare ordering), or None if the set is empty.

  Parameter max_elt : t -> option elt.

Same as min_elt, but returns the largest element of the given set.

End HasOrdOps.

Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps.


Module Type SetsOn (E : OrderedType).
  Include WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder.

  Section Spec.
  Variable s s': t.
  Variable x y : elt.

  Parameter compare_spec : CompSpec eq lt s s' (compare s s').

Additional specification of elements

  Parameter elements_spec2 : sort E.lt (elements s).

Remark: since fold is specified via elements, this stronger specification of elements has an indirect impact on fold, which can now be proved to receive elements in increasing order.

  Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
  Parameter min_elt_spec2 : min_elt s = Some x -> In y s -> ~ E.lt y x.
  Parameter min_elt_spec3 : min_elt s = None -> Empty s.

  Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
  Parameter max_elt_spec2 : max_elt s = Some x -> In y s -> ~ E.lt x y.
  Parameter max_elt_spec3 : max_elt s = None -> Empty s.

Additional specification of choose

  Parameter choose_spec3 : choose s = Some x -> choose s' = Some y ->
    Equal s s' -> E.eq x y.

  End Spec.

End SetsOn.

Static signature for sets on ordered elements

Similar to the functorial signature SetsOn, except that the module E of base elements is incorporated in the signature.

Module Type Sets.
  Declare Module E : OrderedType.
  Include SetsOn E.
End Sets.

Module Type S := Sets.

Some subtyping tests

WSetsOn ---> WSets
 |           |
 |           |
 V           V
SetsOn  ---> Sets

Module S_WS (M : Sets) <: WSets := M.
Module Sfun_WSfun (E:OrderedType)(M : SetsOn E) <: WSetsOn E := M.
Module S_Sfun (M : Sets) <: SetsOn M.E := M.
Module WS_WSfun (M : WSets) <: WSetsOn M.E := M.

Signatures for set representations with ill-formed values.

Motivation:

For many implementation of finite sets (AVL trees, sorted lists, lists without duplicates), we use the same two-layer approach:

A first module deals with the datatype (eg. list or tree) without

any restriction on the values we consider. In this module (named "Raw" in the past), some results are stated under the assumption that some invariant (e.g. sortedness) holds for the input sets. We also prove that this invariant is preserved by set operators.

A second module implements the exact Sets interface by

using a subtype, for instance { l : list A | sorted l }. This module is a mere wrapper around the first Raw module.

With the interfaces below, we give some respectability to the "Raw" modules. This allows the interested users to directly access them via the interfaces. Even better, we can build once and for all a functor doing the transition between Raw and usual Sets.

Description:

The type t of sets may contain ill-formed values on which our set operators may give wrong answers. In particular, mem may not see a element in a ill-formed set (think for instance of a unsorted list being given to an optimized mem that stops its search as soon as a strictly larger element is encountered).

Unlike optimized operators, the In predicate is supposed to always be correct, even on ill-formed sets. Same for Equal and other logical predicates.

A predicate parameter Ok is used to discriminate between well-formed and ill-formed values. Some lemmas hold only on sets validating Ok. This predicate Ok is required to be preserved by set operators. Moreover, a boolean function isok should exist for identifying (at least some of) the well-formed sets.

Module Type WRawSets (E : DecidableType).

First, we ask for all the functions

  Include WOps E.

Is a set well-formed or ill-formed ?

  Parameter IsOk : t -> Prop.
  Class Ok (s:t) : Prop := ok : IsOk s.

In order to be able to validate (at least some) particular sets as well-formed, we ask for a boolean function for (semi-)deciding predicate Ok. If Ok isn't decidable, isok may be the always-false function.

  Parameter isok : t -> bool.

MS: Dangerous instance, the isok s = true hypothesis cannot be discharged with typeclass resolution. Is it really an instance?

  Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.

Logical predicates

  Parameter In : elt -> t -> Prop.
  Declare Instance In_compat : Proper (E.eq==>eq==>iff) In.

  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 : t -> t -> Prop := Equal.
  Declare Instance eq_equiv : Equivalence eq.

First, all operations are compatible with the well-formed predicate.

  Declare Instance empty_ok : Ok empty.
  Declare Instance add_ok s x `(Ok s) : Ok (add x s).
  Declare Instance remove_ok s x `(Ok s) : Ok (remove x s).
  Declare Instance singleton_ok x : Ok (singleton x).
  Declare Instance union_ok s s' `(Ok s, Ok s') : Ok (union s s').
  Declare Instance inter_ok s s' `(Ok s, Ok s') : Ok (inter s s').
  Declare Instance diff_ok s s' `(Ok s, Ok s') : Ok (diff s s').
  Declare Instance filter_ok s f `(Ok s) : Ok (filter f s).
  Declare Instance partition_ok1 s f `(Ok s) : Ok (fst (partition f s)).
  Declare Instance partition_ok2 s f `(Ok s) : Ok (snd (partition f s)).

Now, the specifications, with constraints on the input sets.

  Section Spec.
  Variable s s': t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Parameter mem_spec : forall `{Ok s}, mem x s = true <-> In x s.
  Parameter equal_spec : forall `{Ok s, Ok s'},
    equal s s' = true <-> s[=]s'.
  Parameter subset_spec : forall `{Ok s, Ok s'},
    subset s s' = true <-> s[<=]s'.
  Parameter empty_spec : Empty empty.
  Parameter is_empty_spec : is_empty s = true <-> Empty s.
  Parameter add_spec : forall `{Ok s},
    In y (add x s) <-> E.eq y x \/ In y s.
  Parameter remove_spec : forall `{Ok s},
    In y (remove x s) <-> In y s /\ ~E.eq y x.
  Parameter singleton_spec : In y (singleton x) <-> E.eq y x.
  Parameter union_spec : forall `{Ok s, Ok s'},
    In x (union s s') <-> In x s \/ In x s'.
  Parameter inter_spec : forall `{Ok s, Ok s'},
    In x (inter s s') <-> In x s /\ In x s'.
  Parameter diff_spec : forall `{Ok s, Ok s'},
    In x (diff s s') <-> In x s /\ ~In x s'.
  Parameter fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (flip f) (elements s) i.
  Parameter cardinal_spec : forall `{Ok s},
    cardinal s = length (elements s).
  Parameter filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).
  Parameter for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).
  Parameter exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).
  Parameter partition_spec1 : compatb f ->
    fst (partition f s) [=] filter f s.
  Parameter partition_spec2 : compatb f ->
    snd (partition f s) [=] filter (fun x => negb (f x)) s.
  Parameter elements_spec1 : InA E.eq x (elements s) <-> In x s.
  Parameter elements_spec2w : forall `{Ok s}, NoDupA E.eq (elements s).
  Parameter choose_spec1 : choose s = Some x -> In x s.
  Parameter choose_spec2 : choose s = None -> Empty s.

  End Spec.

End WRawSets.

From weak raw sets to weak usual sets

Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E.

We avoid creating induction principles for the Record

 Local Unset Elimination Schemes.

 Definition elt := E.t.

 Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}.
 Definition t := t_.
 Arguments Mkt this {is_ok}.
 Hint Resolve is_ok : typeclass_instances.

 Definition In (x : elt)(s : t) := M.In x (this s).
 Definition Equal (s s' : t) := forall a : elt, In a s <-> In a s'.
 Definition Subset (s s' : t) := forall a : elt, In a s -> In a s'.
 Definition Empty (s : t) := forall a : elt, ~ In a s.
 Definition For_all (P : elt -> Prop)(s : t) := forall x, In x s -> P x.
 Definition Exists (P : elt -> Prop)(s : t) := exists x, In x s /\ P x.

 Definition mem (x : elt)(s : t) := M.mem x s.
 Definition add (x : elt)(s : t) : t := Mkt (M.add x s).
 Definition remove (x : elt)(s : t) : t := Mkt (M.remove x s).
 Definition singleton (x : elt) : t := Mkt (M.singleton x).
 Definition union (s s' : t) : t := Mkt (M.union s s').
 Definition inter (s s' : t) : t := Mkt (M.inter s s').
 Definition diff (s s' : t) : t := Mkt (M.diff s s').
 Definition equal (s s' : t) := M.equal s s'.
 Definition subset (s s' : t) := M.subset s s'.
 Definition empty : t := Mkt M.empty.
 Definition is_empty (s : t) := M.is_empty s.
 Definition elements (s : t) : list elt := M.elements s.
 Definition choose (s : t) : option elt := M.choose s.
 Definition fold (A : Type)(f : elt -> A -> A)(s : t) : A -> A := M.fold f s.
 Definition cardinal (s : t) := M.cardinal s.
 Definition filter (f : elt -> bool)(s : t) : t := Mkt (M.filter f s).
 Definition for_all (f : elt -> bool)(s : t) := M.for_all f s.
 Definition exists_ (f : elt -> bool)(s : t) := M.exists_ f s.
 Definition partition (f : elt -> bool)(s : t) : t * t :=
   let p := M.partition f s in (Mkt (fst p), Mkt (snd p)).

 Instance In_compat : Proper (E.eq==>eq==>iff) In.Proper (E.eq ==> eq ==> iff) In
 Proof.Proper (E.eq ==> eq ==> iff) In repeat red.forall x y : E.t,
E.eq x y ->
forall x0 y0 : t,
x0 = y0 ->
(In x x0 -> In y y0) /\ (In y y0 -> In x x0) intros; apply M.In_compat; congruence. Qed.

 Definition eq : t -> t -> Prop := Equal.

 Instance eq_equiv : Equivalence eq.Equivalence eq
 Proof.Equivalence eq firstorder. Qed.

 Definition eq_dec : forall (s s':t), { eq s s' }+{ ~eq s s' }.forall s s' : t, {eq s s'} + {~ eq s s'}
 Proof.forall s s' : t, {eq s s'} + {~ eq s s'}
  intros (s,Hs) (s',Hs').s:M.t
Hs:M.Ok s
s':M.t
Hs':M.Ok s'
{eq {| this := s; is_ok := Hs |}
   {| this := s'; is_ok := Hs' |}} +
{~
 eq {| this := s; is_ok := Hs |}
   {| this := s'; is_ok := Hs' |}}
  change ({M.Equal s s'}+{~M.Equal s s'}).s:M.t
Hs:M.Ok s
s':M.t
Hs':M.Ok s'
{M.Equal s s'} + {~ M.Equal s s'}
  destruct (M.equal s s') eqn:H; [left|right];
   rewrite <- M.equal_spec; congruence.
 Defined.


 Section Spec.
  Variable s s' : t.
  Variable x y : elt.
  Variable f : elt -> bool.
  Notation compatb := (Proper (E.eq==>Logic.eq)) (only parsing).

  Lemma mem_spec : mem x s = true <-> In x s.s, s':t
x, y:elt
f:elt -> bool
mem x s = true <-> In x s
  Proof.s, s':t
x, y:elt
f:elt -> bool
mem x s = true <-> In x s exact (@M.mem_spec _ _ _). Qed.
  Lemma equal_spec : equal s s' = true <-> Equal s s'.s, s':t
x, y:elt
f:elt -> bool
equal s s' = true <-> Equal s s'
  Proof.s, s':t
x, y:elt
f:elt -> bool
equal s s' = true <-> Equal s s' exact (@M.equal_spec _ _ _ _). Qed.
  Lemma subset_spec : subset s s' = true <-> Subset s s'.s, s':t
x, y:elt
f:elt -> bool
subset s s' = true <-> Subset s s'
  Proof.s, s':t
x, y:elt
f:elt -> bool
subset s s' = true <-> Subset s s' exact (@M.subset_spec _ _ _ _). Qed.
  Lemma empty_spec : Empty empty.s, s':t
x, y:elt
f:elt -> bool
Empty empty
  Proof.s, s':t
x, y:elt
f:elt -> bool
Empty empty exact M.empty_spec. Qed.
  Lemma is_empty_spec : is_empty s = true <-> Empty s.s, s':t
x, y:elt
f:elt -> bool
is_empty s = true <-> Empty s
  Proof.s, s':t
x, y:elt
f:elt -> bool
is_empty s = true <-> Empty s exact (@M.is_empty_spec _). Qed.
  Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s.s, s':t
x, y:elt
f:elt -> bool
In y (add x s) <-> E.eq y x \/ In y s
  Proof.s, s':t
x, y:elt
f:elt -> bool
In y (add x s) <-> E.eq y x \/ In y s exact (@M.add_spec _ _ _ _). Qed.
  Lemma remove_spec : In y (remove x s) <-> In y s /\ ~E.eq y x.s, s':t
x, y:elt
f:elt -> bool
In y (remove x s) <-> In y s /\ ~ E.eq y x
  Proof.s, s':t
x, y:elt
f:elt -> bool
In y (remove x s) <-> In y s /\ ~ E.eq y x exact (@M.remove_spec _ _ _ _). Qed.
  Lemma singleton_spec : In y (singleton x) <-> E.eq y x.s, s':t
x, y:elt
f:elt -> bool
In y (singleton x) <-> E.eq y x
  Proof.s, s':t
x, y:elt
f:elt -> bool
In y (singleton x) <-> E.eq y x exact (@M.singleton_spec _ _). Qed.
  Lemma union_spec : In x (union s s') <-> In x s \/ In x s'.s, s':t
x, y:elt
f:elt -> bool
In x (union s s') <-> In x s \/ In x s'
  Proof.s, s':t
x, y:elt
f:elt -> bool
In x (union s s') <-> In x s \/ In x s' exact (@M.union_spec _ _ _ _ _). Qed.
  Lemma inter_spec : In x (inter s s') <-> In x s /\ In x s'.s, s':t
x, y:elt
f:elt -> bool
In x (inter s s') <-> In x s /\ In x s'
  Proof.s, s':t
x, y:elt
f:elt -> bool
In x (inter s s') <-> In x s /\ In x s' exact (@M.inter_spec _ _ _ _ _). Qed.
  Lemma diff_spec : In x (diff s s') <-> In x s /\ ~In x s'.s, s':t
x, y:elt
f:elt -> bool
In x (diff s s') <-> In x s /\ ~ In x s'
  Proof.s, s':t
x, y:elt
f:elt -> bool
In x (diff s s') <-> In x s /\ ~ In x s' exact (@M.diff_spec _ _ _ _ _). Qed.
  Lemma fold_spec : forall (A : Type) (i : A) (f : elt -> A -> A),
      fold f s i = fold_left (fun a e => f e a) (elements s) i.s, s':t
x, y:elt
f:elt -> bool
forall (A : Type) (i : A) (f0 : elt -> A -> A),
fold f0 s i =
fold_left (fun (a : A) (e : elt) => f0 e a)
  (elements s) i
  Proof.s, s':t
x, y:elt
f:elt -> bool
forall (A : Type) (i : A) (f0 : elt -> A -> A),
fold f0 s i =
fold_left (fun (a : A) (e : elt) => f0 e a)
  (elements s) i exact (@M.fold_spec _). Qed.
  Lemma cardinal_spec : cardinal s = length (elements s).s, s':t
x, y:elt
f:elt -> bool
cardinal s = length (elements s)
  Proof.s, s':t
x, y:elt
f:elt -> bool
cardinal s = length (elements s) exact (@M.cardinal_spec s _). Qed.
  Lemma filter_spec : compatb f ->
    (In x (filter f s) <-> In x s /\ f x = true).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) <-> In x s /\ f x = true
  Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
In x (filter f s) <-> In x s /\ f x = true exact (@M.filter_spec _ _ _). Qed.
  Lemma for_all_spec : compatb f ->
    (for_all f s = true <-> For_all (fun x => f x = true) s).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = true <->
For_all (fun x0 : elt => f x0 = true) s
  Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
for_all f s = true <->
For_all (fun x0 : elt => f x0 = true) s exact (@M.for_all_spec _ _). Qed.
  Lemma exists_spec : compatb f ->
    (exists_ f s = true <-> Exists (fun x => f x = true) s).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = true <->
Exists (fun x0 : elt => f x0 = true) s
  Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
exists_ f s = true <->
Exists (fun x0 : elt => f x0 = true) s exact (@M.exists_spec _ _). Qed.
  Lemma partition_spec1 : compatb f -> Equal (fst (partition f s)) (filter f s).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Equal (fst (partition f s)) (filter f s)
  Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Equal (fst (partition f s)) (filter f s) exact (@M.partition_spec1 _ _). Qed.
  Lemma partition_spec2 : compatb f ->
      Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Equal (snd (partition f s))
  (filter (fun x0 : elt => negb (f x0)) s)
  Proof.s, s':t
x, y:elt
f:elt -> bool
Proper (E.eq ==> Logic.eq) f ->
Equal (snd (partition f s))
  (filter (fun x0 : elt => negb (f x0)) s) exact (@M.partition_spec2 _ _). Qed.
  Lemma elements_spec1 : InA E.eq x (elements s) <-> In x s.s, s':t
x, y:elt
f:elt -> bool
InA E.eq x (elements s) <-> In x s
  Proof.s, s':t
x, y:elt
f:elt -> bool
InA E.eq x (elements s) <-> In x s exact (@M.elements_spec1 _ _). Qed.
  Lemma elements_spec2w : NoDupA E.eq (elements s).s, s':t
x, y:elt
f:elt -> bool
NoDupA E.eq (elements s)
  Proof.s, s':t
x, y:elt
f:elt -> bool
NoDupA E.eq (elements s) exact (@M.elements_spec2w _ _). Qed.
  Lemma choose_spec1 : choose s = Some x -> In x s.s, s':t
x, y:elt
f:elt -> bool
choose s = Some x -> In x s
  Proof.s, s':t
x, y:elt
f:elt -> bool
choose s = Some x -> In x s exact (@M.choose_spec1 _ _). Qed.
  Lemma choose_spec2 : choose s = None -> Empty s.s, s':t
x, y:elt
f:elt -> bool
choose s = None -> Empty s
  Proof.s, s':t
x, y:elt
f:elt -> bool
choose s = None -> Empty s exact (@M.choose_spec2 _). Qed.

 End Spec.

End WRaw2SetsOn.

Module WRaw2Sets (D:DecidableType)(M:WRawSets D) <: WSets with Module E := D.
  Module E := D.
  Include WRaw2SetsOn D M.
End WRaw2Sets.

Same approach for ordered sets

Module Type RawSets (E : OrderedType).
  Include WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder.

  Section Spec.
  Variable s s': t.
  Variable x y : elt.

Specification of compare

  Parameter compare_spec : forall `{Ok s, Ok s'}, CompSpec eq lt s s' (compare s s').

Additional specification of elements

  Parameter elements_spec2 : forall `{Ok s}, sort E.lt (elements s).

Specification of min_elt

  Parameter min_elt_spec1 : min_elt s = Some x -> In x s.
  Parameter min_elt_spec2 : forall `{Ok s}, min_elt s = Some x -> In y s -> ~ E.lt y x.
  Parameter min_elt_spec3 : min_elt s = None -> Empty s.

Specification of max_elt

  Parameter max_elt_spec1 : max_elt s = Some x -> In x s.
  Parameter max_elt_spec2 : forall `{Ok s}, max_elt s = Some x -> In y s -> ~ E.lt x y.
  Parameter max_elt_spec3 : max_elt s = None -> Empty s.

Additional specification of choose

  Parameter choose_spec3 : forall `{Ok s, Ok s'},
    choose s = Some x -> choose s' = Some y -> Equal s s' -> E.eq x y.

  End Spec.

End RawSets.

From Raw to usual sets

Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
  Include WRaw2SetsOn O M.

  Definition compare (s s':t) := M.compare s s'.
  Definition min_elt (s:t) : option elt := M.min_elt s.
  Definition max_elt (s:t) : option elt := M.max_elt s.
  Definition lt (s s':t) := M.lt s s'.

Specification of lt

  Instance lt_strorder : StrictOrder lt.StrictOrder lt
  Proof.StrictOrder lt constructor ; unfold lt; red.Reflexive (complement (fun s s' : t => M.lt s s'))
forall x y z : t, M.lt x y -> M.lt y z -> M.lt x z
    unfold complement.Reflexive (fun x y : t => M.lt x y -> False)
forall x y z : t, M.lt x y -> M.lt y z -> M.lt x z red.forall x : t, M.lt x x -> False
forall x y z : t, M.lt x y -> M.lt y z -> M.lt x z intros.x:t
H:M.lt x x
False
forall x y z : t, M.lt x y -> M.lt y z -> M.lt x z apply (irreflexivity H).forall x y z : t, M.lt x y -> M.lt y z -> M.lt x z
    intros.x, y, z:t
H:M.lt x y
H0:M.lt y z
M.lt x z transitivity y; auto.
  Qed.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.Proper (eq ==> eq ==> iff) lt
  Proof.Proper (eq ==> eq ==> iff) lt
  repeat red.forall x y : t,
eq x y ->
forall x0 y0 : t,
eq x0 y0 ->
(lt x x0 -> lt y y0) /\ (lt y y0 -> lt x x0) unfold eq, lt.forall x y : t,
Equal x y ->
forall x0 y0 : t,
Equal x0 y0 ->
(M.lt x x0 -> M.lt y y0) /\ (M.lt y y0 -> M.lt x x0)
  intros (s1,p1) (s2,p2) E (s1',p1') (s2',p2') E'; simpl.s1:M.t
p1:M.Ok s1
s2:M.t
p2:M.Ok s2
E:Equal {| this := s1; is_ok := p1 |}
  {| this := s2; is_ok := p2 |}
s1':M.t
p1':M.Ok s1'
s2':M.t
p2':M.Ok s2'
E':Equal {| this := s1'; is_ok := p1' |}
  {| this := s2'; is_ok := p2' |}
(M.lt s1 s1' -> M.lt s2 s2') /\
(M.lt s2 s2' -> M.lt s1 s1')
  change (M.eq s1 s2) in E.s1:M.t
p1:M.Ok s1
s2:M.t
p2:M.Ok s2
E:M.eq s1 s2
s1':M.t
p1':M.Ok s1'
s2':M.t
p2':M.Ok s2'
E':Equal {| this := s1'; is_ok := p1' |}
  {| this := s2'; is_ok := p2' |}
(M.lt s1 s1' -> M.lt s2 s2') /\
(M.lt s2 s2' -> M.lt s1 s1')
  change (M.eq s1' s2') in E'.s1:M.t
p1:M.Ok s1
s2:M.t
p2:M.Ok s2
E:M.eq s1 s2
s1':M.t
p1':M.Ok s1'
s2':M.t
p2':M.Ok s2'
E':M.eq s1' s2'
(M.lt s1 s1' -> M.lt s2 s2') /\
(M.lt s2 s2' -> M.lt s1 s1')
  rewrite E,E'; intuition.
  Qed.

  Section Spec.
  Variable s s' s'' : t.
  Variable x y : elt.

  Lemma compare_spec : CompSpec eq lt s s' (compare s s').s, s', s'':t
x, y:elt
CompSpec eq lt s s' (compare s s')
  Proof.s, s', s'':t
x, y:elt
CompSpec eq lt s s' (compare s s') unfold compare; destruct (@M.compare_spec s s' _ _); auto. Qed.

Additional specification of elements

  Lemma elements_spec2 : sort O.lt (elements s).s, s', s'':t
x, y:elt
Sorted O.lt (elements s)
  Proof.s, s', s'':t
x, y:elt
Sorted O.lt (elements s) exact (@M.elements_spec2 _ _). Qed.

Specification of min_elt

  Lemma min_elt_spec1 : min_elt s = Some x -> In x s.s, s', s'':t
x, y:elt
min_elt s = Some x -> In x s
  Proof.s, s', s'':t
x, y:elt
min_elt s = Some x -> In x s exact (@M.min_elt_spec1 _ _). Qed.
  Lemma min_elt_spec2 : min_elt s = Some x -> In y s -> ~ O.lt y x.s, s', s'':t
x, y:elt
min_elt s = Some x -> In y s -> ~ O.lt y x
  Proof.s, s', s'':t
x, y:elt
min_elt s = Some x -> In y s -> ~ O.lt y x exact (@M.min_elt_spec2 _ _ _ _). Qed.
  Lemma min_elt_spec3 : min_elt s = None -> Empty s.s, s', s'':t
x, y:elt
min_elt s = None -> Empty s
  Proof.s, s', s'':t
x, y:elt
min_elt s = None -> Empty s exact (@M.min_elt_spec3 _). Qed.

Specification of max_elt

  Lemma max_elt_spec1 : max_elt s = Some x -> In x s.s, s', s'':t
x, y:elt
max_elt s = Some x -> In x s
  Proof.s, s', s'':t
x, y:elt
max_elt s = Some x -> In x s exact (@M.max_elt_spec1 _ _). Qed.
  Lemma max_elt_spec2 : max_elt s = Some x -> In y s -> ~ O.lt x y.s, s', s'':t
x, y:elt
max_elt s = Some x -> In y s -> ~ O.lt x y
  Proof.s, s', s'':t
x, y:elt
max_elt s = Some x -> In y s -> ~ O.lt x y exact (@M.max_elt_spec2 _ _ _ _). Qed.
  Lemma max_elt_spec3 : max_elt s = None -> Empty s.s, s', s'':t
x, y:elt
max_elt s = None -> Empty s
  Proof.s, s', s'':t
x, y:elt
max_elt s = None -> Empty s exact (@M.max_elt_spec3 _). Qed.

Additional specification of choose

  Lemma choose_spec3 :
    choose s = Some x -> choose s' = Some y -> Equal s s' -> O.eq x y.s, s', s'':t
x, y:elt
choose s = Some x ->
choose s' = Some y -> Equal s s' -> O.eq x y
  Proof.s, s', s'':t
x, y:elt
choose s = Some x ->
choose s' = Some y -> Equal s s' -> O.eq x y exact (@M.choose_spec3 _ _ _ _ _ _). Qed.

  End Spec.

End Raw2SetsOn.

Module Raw2Sets (O:OrderedType)(M:RawSets O) <: Sets with Module E := O.
  Module E := O.
  Include Raw2SetsOn O M.
End Raw2Sets.

It is in fact possible to provide an ordering on sets with very little information on them (more or less only the In predicate). This generic build of ordering is in fact not used for the moment, we rather use a simpler version dedicated to sets-as-sorted-lists, see MakeListOrdering.

Module Type IN (O:OrderedType).
 Parameter Inline t : Type.
 Parameter Inline In : O.t -> t -> Prop.
 Declare Instance In_compat : Proper (O.eq==>eq==>iff) In.
 Definition Equal s s' := forall x, In x s <-> In x s'.
 Definition Empty s := forall x, ~In x s.
End IN.

Module MakeSetOrdering (O:OrderedType)(Import M:IN O).
 Module Import MO := OrderedTypeFacts O.

 Definition eq : t -> t -> Prop := Equal.

 Instance eq_equiv : Equivalence eq.Equivalence eq
 Proof.Equivalence eq firstorder. Qed.

 Instance : Proper (O.eq==>eq==>iff) In.Proper (O.eq ==> eq ==> iff) In
 Proof.Proper (O.eq ==> eq ==> iff) In
 intros x x' Ex s s' Es.x, x':O.t
Ex:O.eq x x'
s, s':t
Es:eq s s'
In x s <-> In x' s' rewrite Ex.x, x':O.t
Ex:O.eq x x'
s, s':t
Es:eq s s'
In x' s <-> In x' s' apply Es.
 Qed.

 Definition Below x s := forall y, In y s -> O.lt y x.
 Definition Above x s := forall y, In y s -> O.lt x y.

 Definition EquivBefore x s s' :=
   forall y, O.lt y x -> (In y s <-> In y s').

 Definition EmptyBetween x y s :=
   forall z, In z s -> O.lt z y -> O.lt z x.

 Definition lt s s' := exists x, EquivBefore x s s' /\
   ((In x s' /\ Below x s) \/
    (In x s  /\ exists y, In y s' /\ O.lt x y /\ EmptyBetween x y s')).

 Instance : Proper (O.eq==>eq==>eq==>iff) EquivBefore.Proper (O.eq ==> eq ==> eq ==> iff) EquivBefore
 Proof.Proper (O.eq ==> eq ==> eq ==> iff) EquivBefore
  unfold EquivBefore.Proper (O.eq ==> eq ==> eq ==> iff)
  (fun (x : O.t) (s s' : t) =>
   forall y : O.t, O.lt y x -> In y s <-> In y s') intros x x' E s1 s1' E1 s2 s2' E2.x, x':O.t
E:O.eq x x'
s1, s1':t
E1:eq s1 s1'
s2, s2':t
E2:eq s2 s2'
(forall y : O.t, O.lt y x -> In y s1 <-> In y s2) <->
(forall y : O.t, O.lt y x' -> In y s1' <-> In y s2')
  setoid_rewrite E; setoid_rewrite E1; setoid_rewrite E2; intuition.
 Qed.

 Instance : Proper (O.eq==>eq==>iff) Below.Proper (O.eq ==> eq ==> iff) Below
 Proof.Proper (O.eq ==> eq ==> iff) Below
  unfold Below.Proper (O.eq ==> eq ==> iff)
  (fun (x : O.t) (s : t) =>
   forall y : O.t, In y s -> O.lt y x) intros x x' Ex s s' Es.x, x':O.t
Ex:O.eq x x'
s, s':t
Es:eq s s'
(forall y : O.t, In y s -> O.lt y x) <->
(forall y : O.t, In y s' -> O.lt y x')
  setoid_rewrite Ex; setoid_rewrite Es; intuition.
 Qed.

 Instance : Proper (O.eq==>eq==>iff) Above.Proper (O.eq ==> eq ==> iff) Above
 Proof.Proper (O.eq ==> eq ==> iff) Above
  unfold Above.Proper (O.eq ==> eq ==> iff)
  (fun (x : O.t) (s : t) =>
   forall y : O.t, In y s -> O.lt x y) intros x x' Ex s s' Es.x, x':O.t
Ex:O.eq x x'
s, s':t
Es:eq s s'
(forall y : O.t, In y s -> O.lt x y) <->
(forall y : O.t, In y s' -> O.lt x' y)
  setoid_rewrite Ex; setoid_rewrite Es; intuition.
 Qed.

 Instance : Proper (O.eq==>O.eq==>eq==>iff) EmptyBetween.Proper (O.eq ==> O.eq ==> eq ==> iff) EmptyBetween
 Proof.Proper (O.eq ==> O.eq ==> eq ==> iff) EmptyBetween
  unfold EmptyBetween.Proper (O.eq ==> O.eq ==> eq ==> iff)
  (fun (x y : O.t) (s : t) =>
   forall z : O.t, In z s -> O.lt z y -> O.lt z x) intros x x' Ex y y' Ey s s' Es.x, x':O.t
Ex:O.eq x x'
y, y':O.t
Ey:O.eq y y'
s, s':t
Es:eq s s'
(forall z : O.t, In z s -> O.lt z y -> O.lt z x) <->
(forall z : O.t, In z s' -> O.lt z y' -> O.lt z x')
  setoid_rewrite Ex; setoid_rewrite Ey; setoid_rewrite Es; intuition.
 Qed.

 Instance lt_compat : Proper (eq==>eq==>iff) lt.Proper (eq ==> eq ==> iff) lt
 Proof.Proper (eq ==> eq ==> iff) lt
  unfold lt.Proper (eq ==> eq ==> iff)
  (fun s s' : t =>
   exists x : O.t,
     EquivBefore x s s' /\
     (In x s' /\ Below x s \/
      In x s /\
      (exists y : O.t,
         In y s' /\ O.lt x y /\ EmptyBetween x y s'))) intros s1 s1' E1 s2 s2' E2.s1, s1':t
E1:eq s1 s1'
s2, s2':t
E2:eq s2 s2'
(exists x : O.t,
   EquivBefore x s1 s2 /\
   (In x s2 /\ Below x s1 \/
    In x s1 /\
    (exists y : O.t,
       In y s2 /\ O.lt x y /\ EmptyBetween x y s2))) <->
(exists x : O.t,
   EquivBefore x s1' s2' /\
   (In x s2' /\ Below x s1' \/
    In x s1' /\
    (exists y : O.t,
       In y s2' /\ O.lt x y /\ EmptyBetween x y s2')))
  setoid_rewrite E1; setoid_rewrite E2; intuition.
 Qed.

 Instance lt_strorder : StrictOrder lt.StrictOrder lt
 Proof.StrictOrder lt
  split.Irreflexive lt
Transitive lt
  (* irreflexive *)
  intros s (x & _ & [(IN,Em)|(IN & y & IN' & LT & Be)]).s:t
x:O.t
IN:In x s
Em:Below x s
False
s:t
x:O.t
IN:In x s
y:O.t
IN':In y s
LT:O.lt x y
Be:EmptyBetween x y s
False
Transitive lt
  specialize (Em x IN); order.s:t
x:O.t
IN:In x s
y:O.t
IN':In y s
LT:O.lt x y
Be:EmptyBetween x y s
False
Transitive lt
  specialize (Be x IN LT); order.Transitive lt
  (* transitive *)
  intros s1 s2 s3 (x & EQ & [(IN,Pre)|(IN,Lex)])
                  (x' & EQ' & [(IN',Pre')|(IN',Lex')]).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 1) Pre / Pre --> Pre *)
  assert (O.lt x x') by (specialize (Pre' x IN); auto).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  exists x; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
H:O.lt x x'
EquivBefore x s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros y Hy; rewrite <- (EQ' y); auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  left; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
H:O.lt x x'
In x s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  rewrite <- (EQ' x); auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 2) Pre / Lex *)
  elim_compare x x'.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.eq x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 2a) x=x' --> Pre *)
  destruct Lex' as (y & INy & LT & Be).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  exists y; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
EquivBefore y s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:O.lt z y
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 split; intros INz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:O.lt z y
INz:In z s1
In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:O.lt z y
INz:In z s3
In z s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
   specialize (Pre z INz).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
z:O.t
Pre:O.lt z x
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
Hz:O.lt z y
INz:In z s1
In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:O.lt z y
INz:In z s3
In z s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite <- (EQ' z), <- (EQ z); auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:O.lt z y
INz:In z s3
In z s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
   specialize (Be z INz Hz).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
z:O.t
Be:O.lt z x'
H:O.eq x x'
Hz:O.lt z y
INz:In z s3
In z s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite (EQ z), (EQ' z); auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
In y s3 /\ Below y s1 \/
In y s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt y y0 /\ EmptyBetween y y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  left; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
Below y s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y:O.t
INy:In y s3
LT:O.lt x' y
Be:EmptyBetween x' y s3
H:O.eq x x'
z:O.t
Hz:In z s1
O.lt z y
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 transitivity x; auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 2b) x<x' --> Pre *)
  exists x; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
EquivBefore x s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
z:O.t
Hz:O.lt z x
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite <- (EQ' z) by order; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  left; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  rewrite <- (EQ' x); auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 2c) x>x' --> Lex *)
  exists x'; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
EquivBefore x' s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
z:O.t
Hz:O.lt z x'
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite (EQ z) by order; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  right; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Pre:Below x s1
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s1
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  rewrite (EQ x'); auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 3) Lex / Pre --> Lex *)
  destruct Lex as (y & INy & LT & Be).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':Below x' s2
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  specialize (Pre' y INy).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  exists x; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
EquivBefore x s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
z:O.t
Hz:O.lt z x
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite <- (EQ' z) by order; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y0 : O.t,
   In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  right; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  exists y; repeat split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
In y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
EmptyBetween x y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  rewrite <- (EQ' y); auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
EmptyBetween x y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  intros z Hz LTz; apply Be; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s3
Pre':O.lt y x'
z:O.t
Hz:In z s3
LTz:O.lt z y
In z s2
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3 rewrite (EQ' z); auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
lt s1 s3
  (* 4) Lex / Lex *)
  elim_compare x x'.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.eq x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  (* 4a) x=x' --> impossible *)
  destruct Lex as (y & INy & LT & Be).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.eq x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  setoid_replace x with x' in LT; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
Be:EmptyBetween x y s2
x':O.t
LT:O.lt x' y
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.eq x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  specialize (Be x' IN' LT); order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
lt s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  (* 4b) x<x' --> Lex *)
  exists x; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
EquivBefore x s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
z:O.t
Hz:O.lt z x
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 rewrite <- (EQ' z) by order; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
In x s3 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x y /\ EmptyBetween x y s3)
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  right; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x x'
exists y : O.t,
  In y s3 /\ O.lt x y /\ EmptyBetween x y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  destruct Lex as (y & INy & LT & Be).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  elim_compare y x'.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.eq y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   (* 4ba *)
   destruct Lex' as (y' & Iny' & LT' & Be').s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
Be':EmptyBetween x' y' s3
H:O.lt x x'
H0:O.eq y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   exists y'; repeat split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
Be':EmptyBetween x' y' s3
H:O.lt x x'
H0:O.eq y x'
O.lt x y'
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
Be':EmptyBetween x' y' s3
H:O.lt x x'
H0:O.eq y x'
EmptyBetween x y' s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
Be':EmptyBetween x' y' s3
H:O.lt x x'
H0:O.eq y x'
EmptyBetween x y' s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   intros z Hz LTz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
Be':EmptyBetween x' y' s3
H:O.lt x x'
H0:O.eq y x'
z:O.t
Hz:In z s3
LTz:O.lt z y'
O.lt z x
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 specialize (Be' z Hz LTz).s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
z:O.t
Be':O.lt z x'
H:O.lt x x'
H0:O.eq y x'
Hz:In z s3
LTz:O.lt z y'
O.lt z x
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
    rewrite <- (EQ' z) in Hz by order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
z:O.t
Be':O.lt z x'
H:O.lt x x'
H0:O.eq y x'
Hz:In z s2
LTz:O.lt z y'
O.lt z x
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
    apply Be; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
y':O.t
Iny':In y' s3
LT':O.lt x' y'
z:O.t
Be':O.lt z x'
H:O.lt x x'
H0:O.eq y x'
Hz:In z s2
LTz:O.lt z y'
O.lt z y
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   (* 4bb *)
   exists y; repeat split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
In y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
EmptyBetween x y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   rewrite <- (EQ' y); auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
EmptyBetween x y s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   intros z Hz LTz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
z:O.t
Hz:In z s3
LTz:O.lt z y
O.lt z x
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 apply Be; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt y x'
z:O.t
Hz:In z s3
LTz:O.lt z y
In z s2
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 rewrite (EQ' z); auto; order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
   (* 4bc*)
   assert (O.lt x' x) by auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LT:O.lt x y
Be:EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y0 : O.t,
  In y0 s3 /\
  O.lt x' y0 /\ EmptyBetween x' y0 s3
H:O.lt x x'
H0:O.lt x' y
H1:O.lt x' x
exists y0 : O.t,
  In y0 s3 /\ O.lt x y0 /\ EmptyBetween x y0 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3 order.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
lt s1 s3
  (* 4c) x>x' --> Lex *)
  exists x'; split.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
EquivBefore x' s1 s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3)
  intros z Hz.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
z:O.t
Hz:O.lt z x'
In z s1 <-> In z s3
s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t,
  In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3) rewrite (EQ z) by order; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s3 /\ Below x' s1 \/
In x' s1 /\
(exists y : O.t,
   In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3)
  right; split; auto.s1, s2, s3:t
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
Lex:exists y : O.t, In y s2 /\ O.lt x y /\ EmptyBetween x y s2
x':O.t
EQ':EquivBefore x' s2 s3
IN':In x' s2
Lex':exists y : O.t,
  In y s3 /\ O.lt x' y /\ EmptyBetween x' y s3
H:O.lt x' x
In x' s1
  rewrite (EQ x'); auto.
 Qed.

 Lemma lt_empty_r : forall s s', Empty s' -> ~ lt s s'.forall s s' : t, Empty s' -> ~ lt s s'
 Proof.forall s s' : t, Empty s' -> ~ lt s s'
  intros s s' Hs' (x & _ & [(IN,_)|(_ & y & IN & _)]).s, s':t
Hs':Empty s'
x:O.t
IN:In x s'
False
s, s':t
Hs':Empty s'
x, y:O.t
IN:In y s'
False
  elim (Hs' x IN).s, s':t
Hs':Empty s'
x, y:O.t
IN:In y s'
False
  elim (Hs' y IN).
 Qed.

 Definition Add x s s' := forall y, In y s' <-> O.eq x y \/ In y s.

 Lemma lt_empty_l : forall x s1 s2 s2',
  Empty s1 -> Above x s2 -> Add x s2 s2' -> lt s1 s2'.forall (x : O.t) (s1 s2 s2' : t),
Empty s1 -> Above x s2 -> Add x s2 s2' -> lt s1 s2'
 Proof.forall (x : O.t) (s1 s2 s2' : t),
Empty s1 -> Above x s2 -> Add x s2 s2' -> lt s1 s2'
  intros x s1 s2 s2' Em Ab Ad.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
lt s1 s2'
  exists x; split.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
EquivBefore x s1 s2'
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  intros y Hy; split; intros IN.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
IN:In y s1
In y s2'
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
IN:In y s2'
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  elim (Em y IN).x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
IN:In y s2'
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  rewrite (Ad y) in IN; destruct IN as [EQ|IN].x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
EQ:O.eq x y
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
IN:In y s2
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2') order.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:O.lt y x
IN:In y s2
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  specialize (Ab y IN).x:O.t
s1, s2, s2':t
Em:Empty s1
y:O.t
Ab:O.lt x y
Ad:Add x s2 s2'
Hy:O.lt y x
IN:In y s2
In y s1
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2') order.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2' /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  left; split.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
In x s2'
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
Below x s1
  rewrite (Ad x).x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
O.eq x x \/ In x s2
x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
Below x s1 now left.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
Below x s1
  intros y Hy.x:O.t
s1, s2, s2':t
Em:Empty s1
Ab:Above x s2
Ad:Add x s2 s2'
y:O.t
Hy:In y s1
O.lt y x elim (Em y Hy).
 Qed.

 Lemma lt_add_lt : forall x1 x2 s1 s1' s2 s2',
   Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' ->
   O.lt x1 x2 -> lt s1' s2'.forall (x1 x2 : O.t) (s1 s1' s2 s2' : t),
Above x1 s1 ->
Above x2 s2 ->
Add x1 s1 s1' ->
Add x2 s2 s2' -> O.lt x1 x2 -> lt s1' s2'
  Proof.forall (x1 x2 : O.t) (s1 s1' s2 s2' : t),
Above x1 s1 ->
Above x2 s2 ->
Add x1 s1 s1' ->
Add x2 s2 s2' -> O.lt x1 x2 -> lt s1' s2'
  intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 LT.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
lt s1' s2'
  exists x1; split; [ | right; split]; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
EquivBefore x1 s1' s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  intros y Hy.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
In y s1' <-> In y s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2' rewrite (Ad1 y), (Ad2 y).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
O.eq x1 y \/ In y s1 <-> O.eq x2 y \/ In y s2
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  split; intros [U|U]; try order.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
U:In y s1
O.eq x2 y \/ In y s2
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
U:In y s2
O.eq x1 y \/ In y s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  specialize (Ab1 y U).x1, x2:O.t
s1, s1', s2, s2':t
y:O.t
Ab1:O.lt x1 y
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
Hy:O.lt y x1
U:In y s1
O.eq x2 y \/ In y s2
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
U:In y s2
O.eq x1 y \/ In y s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2' order.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
Hy:O.lt y x1
U:In y s2
O.eq x1 y \/ In y s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  specialize (Ab2 y U).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
y:O.t
Ab2:O.lt x2 y
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
Hy:O.lt y x1
U:In y s2
O.eq x1 y \/ In y s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2' order.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x1 s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  rewrite (Ad1 x1); auto with *.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
exists y : O.t,
  In y s2' /\ O.lt x1 y /\ EmptyBetween x1 y s2'
  exists x2; repeat split; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
In x2 s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
EmptyBetween x1 x2 s2'
  rewrite (Ad2 x2); now left.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
EmptyBetween x1 x2 s2'
  intros y.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
In y s2' -> O.lt y x2 -> O.lt y x1 rewrite (Ad2 y).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
O.eq x2 y \/ In y s2 -> O.lt y x2 -> O.lt y x1 intros [U|U].x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
U:O.eq x2 y
O.lt y x2 -> O.lt y x1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
U:In y s2
O.lt y x2 -> O.lt y x1 order.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
y:O.t
U:In y s2
O.lt y x2 -> O.lt y x1
  specialize (Ab2 y U).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
y:O.t
Ab2:O.lt x2 y
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
LT:O.lt x1 x2
U:In y s2
O.lt y x2 -> O.lt y x1 order.
  Qed.

  Lemma lt_add_eq : forall x1 x2 s1 s1' s2 s2',
   Above x1 s1 -> Above x2 s2 -> Add x1 s1 s1' -> Add x2 s2 s2' ->
   O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'.forall (x1 x2 : O.t) (s1 s1' s2 s2' : t),
Above x1 s1 ->
Above x2 s2 ->
Add x1 s1 s1' ->
Add x2 s2 s2' -> O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'
  Proof.forall (x1 x2 : O.t) (s1 s1' s2 s2' : t),
Above x1 s1 ->
Above x2 s2 ->
Add x1 s1 s1' ->
Add x2 s2 s2' -> O.eq x1 x2 -> lt s1 s2 -> lt s1' s2'
  intros x1 x2 s1 s1' s2 s2' Ab1 Ab2 Ad1 Ad2 Hx (x & EQ & Disj).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
lt s1' s2'
  assert (O.lt x1 x).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
O.lt x1 x
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
lt s1' s2'
   destruct Disj as [(IN,_)|(IN,_)]; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
O.lt x1 x
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
lt s1' s2' rewrite Hx; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
lt s1' s2'
  exists x; split.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
EquivBefore x s1' s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  intros z Hz.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
z:O.t
Hz:O.lt z x
In z s1' <-> In z s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2') rewrite (Ad1 z), (Ad2 z).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
z:O.t
Hz:O.lt z x
O.eq x1 z \/ In z s1 <-> O.eq x2 z \/ In z s2
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  split; intros [U|U]; try (left; order); right.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
z:O.t
Hz:O.lt z x
U:In z s1
In z s2
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
z:O.t
Hz:O.lt z x
U:In z s2
In z s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  rewrite <- (EQ z); auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
z:O.t
Hz:O.lt z x
U:In z s2
In z s1
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  rewrite (EQ z); auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
Disj:In x s2 /\ Below x s1 \/
In x s1 /\
(exists y : O.t,
   In y s2 /\ O.lt x y /\ EmptyBetween x y s2)
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
  destruct Disj as [(IN,Em)|(IN & y & INy & LTy & Be)].x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Em:Below x s1
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y : O.t,
   In y s2' /\ O.lt x y /\ EmptyBetween x y s2')
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y0 : O.t,
   In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2')
  left; split; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Em:Below x s1
H:O.lt x1 x
In x s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Em:Below x s1
H:O.lt x1 x
Below x s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y0 : O.t,
   In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2')
  rewrite (Ad2 x); auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Em:Below x s1
H:O.lt x1 x
Below x s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y0 : O.t,
   In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2')
  intros z.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s2
Em:Below x s1
H:O.lt x1 x
z:O.t
In z s1' -> O.lt z x
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y0 : O.t,
   In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2') rewrite (Ad1 z); intros [U|U]; try specialize (Ab1 z U); auto; order.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s2' /\ Below x s1' \/
In x s1' /\
(exists y0 : O.t,
   In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2')
  right; split; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In x s1'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
exists y0 : O.t,
  In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2'
  rewrite (Ad1 x); auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
exists y0 : O.t,
  In y0 s2' /\ O.lt x y0 /\ EmptyBetween x y0 s2'
  exists y; repeat split; auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
In y s2'
x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
EmptyBetween x y s2'
  rewrite (Ad2 y); auto.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
EmptyBetween x y s2'
  intros z.x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
z:O.t
In z s2' -> O.lt z y -> O.lt z x rewrite (Ad2 z).x1, x2:O.t
s1, s1', s2, s2':t
Ab1:Above x1 s1
Ab2:Above x2 s2
Ad1:Add x1 s1 s1'
Ad2:Add x2 s2 s2'
Hx:O.eq x1 x2
x:O.t
EQ:EquivBefore x s1 s2
IN:In x s1
y:O.t
INy:In y s2
LTy:O.lt x y
Be:EmptyBetween x y s2
H:O.lt x1 x
z:O.t
O.eq x2 z \/ In z s2 -> O.lt z y -> O.lt z x intros [U|U]; try specialize (Ab2 z U); auto; order.
  Qed.

End MakeSetOrdering.


Module MakeListOrdering (O:OrderedType).
 Module MO:=OrderedTypeFacts O.

 Notation t := (list O.t).
 Notation In := (InA O.eq).

 Definition eq s s' := forall x, In x s <-> In x s'.

 Instance eq_equiv : Equivalence eq := _.

 Inductive lt_list : t -> t -> Prop :=
    | lt_nil : forall x s, lt_list nil (x :: s)
    | lt_cons_lt : forall x y s s',
        O.lt x y -> lt_list (x :: s) (y :: s')
    | lt_cons_eq : forall x y s s',
        O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
 Hint Constructors lt_list : core.

 Definition lt := lt_list.
 Hint Unfold lt : core.

 Instance lt_strorder : StrictOrder lt.StrictOrder lt
 Proof.StrictOrder lt
 split.Irreflexive lt
Transitive lt
 (* irreflexive *)
 assert (forall s s', s=s' -> ~lt s s').forall s s' : t, s = s' -> ~ lt s s'
H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
  red; induction 2.x:O.t
s:t
H:nil = x :: s
False
x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.lt x y
False
x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.eq x y
H1:lt_list s s'
IHlt_list:s = s' -> False
False
H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
  discriminate.x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.lt x y
False
x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.eq x y
H1:lt_list s s'
IHlt_list:s = s' -> False
False
H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
  inversion H; subst.y:O.t
s':t
H0:O.lt y y
H:y :: s' = y :: s'
False
x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.eq x y
H1:lt_list s s'
IHlt_list:s = s' -> False
False
H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
  apply (StrictOrder_Irreflexive y); auto.x, y:O.t
s, s':t
H:x :: s = y :: s'
H0:O.eq x y
H1:lt_list s s'
IHlt_list:s = s' -> False
False
H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
  inversion H; subst; auto.H:forall s s' : t, s = s' -> ~ lt s s'
Irreflexive lt
Transitive lt
 intros s Hs; exact (H s s (eq_refl s) Hs).Transitive lt
 (* transitive *)
 intros s s' s'' H; generalize s''; clear s''; elim H.s, s':t
H:lt s s'
forall (x : O.t) (s0 s'' : t),
lt (x :: s0) s'' -> lt nil s''
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.lt x y ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
 intros x l s'' H'; inversion_clear H'; auto.s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.lt x y ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
 intros x x' l l' E s'' H'; inversion_clear H'; auto.s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.lt x' y
lt (x :: l) (y :: s'0)
s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.eq x' y
H1:lt_list l' s'0
lt (x :: l) (y :: s'0)
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
 constructor 2.s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.lt x' y
O.lt x y
s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.eq x' y
H1:lt_list l' s'0
lt (x :: l) (y :: s'0)
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s'' transitivity x'; auto.s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.eq x' y
H1:lt_list l' s'0
lt (x :: l) (y :: s'0)
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
 constructor 2.s, s':t
H:lt s s'
x, x':O.t
l, l':t
E:O.lt x x'
s'':t
y:O.t
s'0:t
H0:O.eq x' y
H1:lt_list l' s'0
O.lt x y
s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s'' rewrite <- H0; auto.s, s':t
H:lt s s'
forall (x y : O.t) (s0 s'0 : t),
O.eq x y ->
lt_list s0 s'0 ->
(forall s'' : t, lt s'0 s'' -> lt s0 s'') ->
forall s'' : t, lt (y :: s'0) s'' -> lt (x :: s0) s''
 intros.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
H3:lt (y :: s'0) s''
lt (x :: s0) s''
 inversion_clear H3.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.lt y y0
lt (x :: s0) (y0 :: s'1)
s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
lt (x :: s0) (y0 :: s'1)
 constructor 2.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.lt y y0
O.lt x y0
s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
lt (x :: s0) (y0 :: s'1) rewrite H0; auto.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
lt (x :: s0) (y0 :: s'1)
 constructor 3; auto.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
O.eq x y0
s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
lt_list s0 s'1 transitivity y; auto.s, s':t
H:lt s s'
x, y:O.t
s0, s'0:t
H0:O.eq x y
H1:lt_list s0 s'0
H2:forall s''0 : t, lt s'0 s''0 -> lt s0 s''0
s'':t
y0:O.t
s'1:t
H4:O.eq y y0
H5:lt_list s'0 s'1
lt_list s0 s'1 unfold lt in *; auto.
 Qed.

 Instance lt_compat' :
  Proper (eqlistA O.eq==>eqlistA O.eq==>iff) lt.Proper (eqlistA O.eq ==> eqlistA O.eq ==> iff) lt
 Proof.Proper (eqlistA O.eq ==> eqlistA O.eq ==> iff) lt
 apply proper_sym_impl_iff_2; auto with *.Proper (eqlistA O.eq ==> eqlistA O.eq ==> impl) lt
 intros s1 s1' E1 s2 s2' E2 H.s1, s1':t
E1:eqlistA O.eq s1 s1'
s2, s2':t
E2:eqlistA O.eq s2 s2'
H:lt s1 s2
lt s1' s2'
 revert s1' E1 s2' E2.s1, s2:t
H:lt s1 s2
forall s1' : t,
eqlistA O.eq s1 s1' ->
forall s2' : t, eqlistA O.eq s2 s2' -> lt s1' s2'
 induction H; intros; inversion_clear E1; inversion_clear E2.x:O.t
s, s1', s2':t
x':O.t
l':t
H:O.eq x x'
H0:eqlistA O.eq s l'
lt nil (x' :: l')
x, y:O.t
s, s':t
H:O.lt x y
s1', s2':t
x':O.t
l':t
H0:O.eq x x'
H1:eqlistA O.eq s l'
x'0:O.t
l'0:t
H2:O.eq y x'0
H3:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0)
x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0)
 constructor 1.x, y:O.t
s, s':t
H:O.lt x y
s1', s2':t
x':O.t
l':t
H0:O.eq x x'
H1:eqlistA O.eq s l'
x'0:O.t
l'0:t
H2:O.eq y x'0
H3:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0)
x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0)
 constructor 2.x, y:O.t
s, s':t
H:O.lt x y
s1', s2':t
x':O.t
l':t
H0:O.eq x x'
H1:eqlistA O.eq s l'
x'0:O.t
l'0:t
H2:O.eq y x'0
H3:eqlistA O.eq s' l'0
O.lt x' x'0
x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0) MO.order.x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt (x' :: l') (x'0 :: l'0)
 constructor 3.x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
O.eq x' x'0
x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt_list l' l'0 MO.order.x, y:O.t
s, s':t
H:O.eq x y
H0:lt_list s s'
IHlt_list:forall s1'0 : t,
eqlistA O.eq s s1'0 ->
forall s2'0 : t,
eqlistA O.eq s' s2'0 -> lt s1'0 s2'0
s1', s2':t
x':O.t
l':t
H1:O.eq x x'
H2:eqlistA O.eq s l'
x'0:O.t
l'0:t
H3:O.eq y x'0
H4:eqlistA O.eq s' l'0
lt_list l' l'0 unfold lt in *; auto.
 Qed.

 Lemma eq_cons :
  forall l1 l2 x y,
  O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2).forall (l1 l2 : t) (x y : O.t),
O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2)
 Proof.forall (l1 l2 : t) (x y : O.t),
O.eq x y -> eq l1 l2 -> eq (x :: l1) (y :: l2)
  unfold eq; intros l1 l2 x y Exy E12 z.l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
In z (x :: l1) <-> In z (y :: l2)
  split; inversion_clear 1.l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:O.eq z x
In z (y :: l2)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l1
In z (y :: l2)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:O.eq z y
In z (x :: l1)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l2
In z (x :: l1)
  left; MO.order.l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l1
In z (y :: l2)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:O.eq z y
In z (x :: l1)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l2
In z (x :: l1) right; rewrite <- E12; auto.l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:O.eq z y
In z (x :: l1)
l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l2
In z (x :: l1)
  left; MO.order.l1, l2:t
x, y:O.t
Exy:O.eq x y
E12:forall x0 : O.t, In x0 l1 <-> In x0 l2
z:O.t
H0:In z l2
In z (x :: l1) right; rewrite E12; auto.
 Qed.
 Hint Resolve eq_cons : core.

 Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
  CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.forall (c : comparison) (x1 x2 : O.t) (l1 l2 : t),
O.eq x1 x2 ->
CompSpec eq lt l1 l2 c ->
CompSpec eq lt (x1 :: l1) (x2 :: l2) c
 Proof.forall (c : comparison) (x1 x2 : O.t) (l1 l2 : t),
O.eq x1 x2 ->
CompSpec eq lt l1 l2 c ->
CompSpec eq lt (x1 :: l1) (x2 :: l2) c
  destruct c; simpl; inversion_clear 2; auto with relations.
 Qed.
 Hint Resolve cons_CompSpec : core.

End MakeListOrdering.