Require Import Arith.
Require Export List.
Require Import Lexicographic_Exponentiation.
Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Export Option.
Require Export sTactic.
Section OrderedList.

Variable A : Set.
Variable ltA : A → A → Prop.
Variable eqA : A → A → Prop.
Hypothesis eqARefl : reflexive A eqA.
Hypothesis eqASym : symmetric A eqA.
Hypothesis eqATrans : transitive A eqA.
Hypothesis ltADec : ∀ a b : A, {ltA a b} + {ltA b a} + {eqA a b}.
Hypothesis ltATrans : transitive A ltA.
Hypothesis ltAAnti : ∀ a : A, ¬ ltA a a.
Hypothesis ltAImpNotEqA : ∀ a b : A, ltA a b → ¬ eqA a b.
Hypothesis ltAntiSym : ∀ a b : A, ltA a b → ¬ ltA b a.
Variable f : A → A.
Hypothesis feqA : ∀ a : A, eqA (f a) a.
Hypothesis
  ltAeqAComp : ∀ a b c d : A, ltA a b → eqA a c → eqA b d → ltA c d.

Definition eqADec : ∀ a b : A, {eqA a b} + {¬ eqA a b}.
intros a b; case (ltADec a b); intros Test; auto.
Casec Test; intros Test; auto.
right.
red in |- *; intros H'; absurd (eqA b a); auto.
Qed.
Hypothesis eqADec' : ∀ a b : A, {eqA a b} + {¬ eqA a b}.

Inductive Olist : list A → Prop :=
  | OlistNil : Olist nil
  | OlistOne : ∀ a : A, Olist (a :: nil)
  | OlistCons :
      ∀ (a b : A) (L : list A),
      Olist (b :: L) → ltA a b → Olist (a :: b :: L).
Hint Resolve OlistNil OlistOne OlistCons.

Theorem OlistInv : ∀ (a : A) (L : list A), Olist (a :: L) → Olist L.
intros a L H'; inversion H'; auto.
Qed.

Theorem OlistSkip :
 ∀ (a b : A) (L : list A), Olist (a :: b :: L) → Olist (a :: L).
intros a b L; case L.
intros H'.
apply OlistOne; auto.
intros a0 l; case l.
intros H'.
apply OlistCons; auto.
apply ltATrans with (y := b); auto.
inversion H'; auto.
inversion H'; auto.
inversion H1; auto.
intros a1 l0 H'; inversion H'; inversion H1.
apply OlistCons; auto.
apply ltATrans with (y := b); auto.
Qed.

Theorem OlistSup :
 ∀ (a : A) (L : list A),
 Olist (a :: L) → ∀ b : A, In b L → ltA a b.
intros a L; elim L; simpl in |- *; auto.
intros H' b H'0; elim H'0.
intros a0 l H' H'0 b H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ];
 auto.
inversion H'0; auto.
apply H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem OlistUnique :
 ∀ (L : list A) (a b : A), Olist (a :: L) → eqA a b → ¬ In b L.
intros L a b H' H'0; red in |- *; intros H'1; absurd (eqA a b); auto.
apply ltAImpNotEqA; auto.
apply OlistSup with (L := L); auto.
Qed.

Theorem OlistIn :
 ∀ (L : list A) (a b : A),
 In a L → In b L → Olist L → eqA a b → a = b.
intros L; elim L; simpl in |- *; auto.
intros a b H'; elim H'; auto.
intros a l H' a0 b H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ].
intros H'1; Casec H'1; intros H'1; auto.
intros H'2 H'3; absurd (eqA a b); auto.
apply ltAImpNotEqA; auto.
apply OlistSup with (L := l); auto.
intros H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ]; intros H'2 H'3.
absurd (eqA a a0); auto.
apply ltAImpNotEqA; auto.
apply OlistSup with (L := l); auto.
apply H'; auto.
apply OlistInv with (a := a); auto.
Qed.

Inductive InEq : A → list A → Prop :=
  | InEqHead : ∀ (a b : A) (L : list A), eqA a b → InEq a (b :: L)
  | InEqSkip : ∀ (a b : A) (L : list A), InEq a L → InEq a (b :: L).
Hint Resolve InEqHead InEqSkip.

Definition InEqDec :
  ∀ (a : A) (L1 : list A), {InEq a L1} + {¬ InEq a L1}.
fix 2.
intros a L1; case L1.
right; red in |- *; intros H'; inversion H'; auto.
intros a0 l; case (eqADec' a a0); intros Eqaa0.
left; auto.
case (InEqDec a l); intros REc.
left; auto.
right; red in |- *; intros H'0; inversion H'0; auto.
Defined.

Theorem inImpInEq : ∀ (a : A) (L : list A), In a L → InEq a L.
intros a L; elim L; simpl in |- *; auto.
intros H'; elim H'.
intros a0 l H' H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ]; auto.
Qed.

Theorem OlistSupEq :
 ∀ (a : A) (L : list A),
 Olist (a :: L) → ∀ b : A, InEq b L → ltA a b.
intros a L; elim L; simpl in |- *; auto.
intros H' b H'0; inversion H'0.
intros a0 l H' H'0 b H'1; inversion_clear H'1.
apply ltAeqAComp with (a := a) (b := a0); auto.
apply OlistSup with (L := a0 :: l); simpl in |- *; auto.
apply H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem OlistUniqueEq :
 ∀ (L : list A) (a b : A), Olist (a :: L) → eqA a b → ¬ InEq b L.
intros L a b H' H'0; red in |- *; intros H'1; absurd (eqA a b); auto.
apply ltAImpNotEqA; auto.
apply OlistSupEq with (L := L); auto.
Qed.

Theorem InEqComp :
 ∀ (a b : A) (L : list A), InEq a L → eqA a b → InEq b L.
intros a b L H'; generalize b; clear b; elim H'; auto.
intros a0 b L0 H'0 b0 H'1.
apply InEqHead; auto.
apply eqATrans with (y := a0); auto.
Qed.

Theorem NotInEqComp :
 ∀ (a b : A) (L : list A), ¬ InEq a L → eqA a b → ¬ InEq b L.
intros a b L H' H'0; red in |- *; intros H'1; case H'; auto.
apply InEqComp with (a := b); auto.
Qed.

Inductive InclEq : list A → list A → Prop :=
    InclEqDef :
      ∀ L1 L2 : list A,
      (∀ a : A, InEq a L1 → InEq a L2) → InclEq L1 L2.
Hint Resolve InclEqDef.

Theorem inclImpImplEq : ∀ L1 L2 : list A, incl L1 L2 → InclEq L1 L2.
intros L1 L2 H'; apply InclEqDef.
intros a H'0; generalize H'; elim H'0; auto.
intros a0 b L H'1 H'2.
apply InEqComp with (a := b); auto.
apply inImpInEq; auto with datatypes.
intros a0 b L H'1 H'2 H'3.
apply H'2; auto.
apply incl_tran with (A := A) (m := b :: L); auto with datatypes.
Qed.

Theorem InclEqNil : ∀ L : list A, InclEq nil L.
intros L.
apply InclEqDef; auto.
intros a H'; inversion H'.
Qed.
Hint Resolve InclEqNil.

Theorem InclEqRef : ∀ L : list A, InclEq L L.
intros L.
apply InclEqDef; auto.
Qed.
Hint Resolve InclEqRef.

Theorem InclEqTrans : transitive (list A) InclEq.
red in |- ×.
intros x y z H' H'0; inversion_clear H'; inversion_clear H'0; auto.
Qed.

Theorem InclEqCons :
 ∀ (a : A) (L1 L2 : list A),
 InEq a L2 → InclEq L1 L2 → InclEq (a :: L1) L2.
intros a L1 L2 H' H'0; inversion H'0; auto.
apply InclEqDef; auto.
intros a0 H'1; inversion H'1; auto.
apply InEqComp with (a := a); auto.
Qed.
Hint Resolve InclEqCons.

Inductive EqL : list A → list A → Prop :=
  | EqLNil : EqL nil nil
  | EqLCons :
      ∀ (a b : A) (L1 L2 : list A),
      eqA a b → EqL L1 L2 → EqL (a :: L1) (b :: L2).
Hint Resolve EqLNil EqLCons.

Theorem EqLInv :
 ∀ (L1 L2 : list A) (a : A), EqL L1 L2 → InEq a L1 → InEq a L2.
intros L1 L2 a H'; elim H'; auto.
intros a0 b L3 L4 H'0 H'1 H'2 H'3; inversion H'3; auto.
apply InEqHead; auto.
apply eqATrans with (y := a0); auto.
Qed.

Theorem EqLRef : ∀ L : list A, EqL L L.
intros L; elim L; auto.
Qed.
Hint Resolve EqLRef.

Theorem EqLTrans : ∀ L : list A, transitive (list A) EqL.
intros L; red in |- ×.
intros x y z H'; generalize z; Elimc H'; clear z; auto.
intros a b L1 L2 H' H'0 H'1 z H'2; inversion H'2; auto.
apply EqLCons; auto.
apply eqATrans with (y := b); auto.
Qed.

Theorem InclEqOlist :
 ∀ (L1 L2 : list A) (a b : A),
 Olist (a :: L1) →
 Olist (b :: L2) → InclEq (a :: L1) (b :: L2) → InclEq L1 L2.
intros L1 L2 a b H' H'0 H'1.
apply InclEqDef; auto.
intros a0 H'2.
inversion H'1.
lapply (H a0); [ intros H'4; inversion H'4 | try assumption ]; auto.
cut (ltA a a0); auto.
2: apply OlistSupEq with (L := L1); auto.
intros H'3.
lapply (H a); [ intros H'6; inversion H'6 | idtac ]; auto.
absurd (eqA a b); auto.
apply ltAImpNotEqA; auto.
apply ltAeqAComp with (a := a) (b := a0); auto.
absurd (ltA b a); auto.
apply ltAntiSym; auto.
apply ltAeqAComp with (a := a) (b := a0); auto.
apply OlistSupEq with (L := L2); auto.
Qed.

Theorem EqLOlist :
 ∀ L1 L2 : list A,
 Olist L1 → Olist L2 → InclEq L1 L2 → InclEq L2 L1 → EqL L1 L2.
intros L1; elim L1; auto.
intros L2; case L2; auto.
intros a l H' H'0 H'1 H'2; inversion H'2.
lapply (H a); [ intros H'4; inversion H'4 | idtac ]; auto.
intros a l H' L2; case L2; auto.
intros H'0 H'1 H'2; inversion H'2.
lapply (H a); [ intros H'4; inversion H'4 | idtac ]; auto.
intros a0 l0 H'0 H'1 H'2 H'3; auto.
apply EqLCons; auto.
2: apply H'; auto.
2: apply OlistInv with (a := a); auto.
2: apply OlistInv with (a := a0); auto.
2: apply InclEqOlist with (a := a) (b := a0); auto.
2: apply InclEqOlist with (a := a0) (b := a); auto.
inversion H'3.
lapply (H a0); [ intros H'5; inversion H'5 | idtac ]; auto.
inversion H'2; auto.
lapply (H6 a); [ intros H'6; inversion H'6 | idtac ]; auto.
absurd (ltA a0 a); auto.
apply ltAntiSym; auto.
apply OlistSupEq with (L := l); auto.
apply OlistSupEq with (L := l0); auto.
Qed.

Fixpoint diffElem (L1 : list A) : list A → Option A :=
  fun L2 : list A ⇒
  match L1 with
  | nil ⇒ None _
  | a :: L'1 ⇒
      match InEqDec a L2 with
      | left _ ⇒ diffElem L'1 L2
      | right _ ⇒ Some _ a
      end
  end.

Theorem diffElemNone :
 ∀ L1 L2 : list A, diffElem L1 L2 = None _ → InclEq L1 L2.
intros L1; elim L1; simpl in |- *; auto.
intros a l H' L2.
case (InEqDec a L2); auto.
intros H'0 H'1; discriminate.
Qed.

Theorem diffElemSomeIn :
 ∀ (L1 L2 : list A) (a : A), diffElem L1 L2 = Some _ a → InEq a L1.
intros L1; elim L1; simpl in |- *; auto.
intros H' a H'0; discriminate.
intros a l H' L2 a0.
case (InEqDec a L2); intros InEq0 Eq0; auto.
apply InEqSkip; auto.
apply H' with (L2 := L2); auto.
inversion Eq0; auto.
Qed.

Theorem diffElemSomeNIn :
 ∀ (L1 L2 : list A) (a : A), diffElem L1 L2 = Some _ a → ¬ InEq a L2.
intros L1; elim L1; simpl in |- *; auto.
intros H' a H'0; discriminate.
intros a l H' L2 a0.
case (InEqDec a L2); intros InEq0 Eq0; auto.
inversion Eq0; auto.
rewrite <- H0; auto.
Qed.

Definition olistDiff :
  ∀ L1 L2 : list A,
  Olist L1 →
  Olist L2 →
  ¬ EqL L1 L2 →
  {a : A | InEq a L1 ∧ ¬ InEq a L2 ∨ ¬ InEq a L1 ∧ InEq a L2}.
intros L1 L2 H' H'0 H'1.
generalize (refl_equal (diffElem L1 L2));
 pattern (diffElem L1 L2) at -1 in |- *; case (diffElem L1 L2);
 auto.
intros x H'2; ∃ x; left; split; auto.
apply diffElemSomeIn with (1 := H'2); auto.
apply diffElemSomeNIn with (1 := H'2); auto.
intros Eq1.
generalize (refl_equal (diffElem L2 L1));
 pattern (diffElem L2 L1) at -1 in |- *; case (diffElem L2 L1);
 auto.
intros x H'2; ∃ x; right; split; auto.
apply diffElemSomeNIn with (1 := H'2); auto.
apply diffElemSomeIn with (1 := H'2); auto.
intros Eq2; absurd (EqL L1 L2); auto.
apply EqLOlist; auto.
apply diffElemNone; auto.
apply diffElemNone; auto.
Defined.

Inductive Disjoint : list A → list A → Prop :=
    DisjointDef :
      ∀ L1 L2 : list A,
      (∀ a : A, InEq a L1 → ¬ InEq a L2) → Disjoint L1 L2.

Theorem DisjointCom : ∀ L1 L2 : list A, Disjoint L1 L2 → Disjoint L2 L1.
intros L1 L2 H'; elim H'; auto.
intros L3 L4 H'0.
apply DisjointDef.
intros a H'1; red in |- *; intros H'2; absurd (InEq a L4); auto.
Qed.

Theorem DisjointInv1 :
 ∀ (a : A) (L1 L2 : list A), Disjoint L1 (a :: L2) → Disjoint L1 L2.
intros a L1 L2 H'; inversion H'; apply DisjointDef.
intros a0 H'0; red in |- *; intros H'1.
lapply (H a0); [ intros H'3; apply H'3 | idtac ]; auto.
Qed.

Theorem DisjointInv2 :
 ∀ (a : A) (L1 L2 : list A), Disjoint (a :: L1) L2 → Disjoint L1 L2.
intros a L1 L2 H'.
apply DisjointCom.
apply DisjointInv1 with (a := a); auto.
apply DisjointCom; auto.
Qed.

Theorem DisjointCons1 :
 ∀ (b : A) (L1 L2 : list A),
 Disjoint L1 L2 → ¬ InEq b L1 → Disjoint L1 (b :: L2).
intros a L1 L2 H' H'0; inversion_clear H'.
apply DisjointDef; simpl in |- *; auto.
intros b H'1; red in |- *; intros H'2; inversion_clear H'2; auto.
case H'0; apply InEqComp with (a := b); auto.
absurd (InEq b L2); auto.
Qed.

Theorem DisjointCons2 :
 ∀ (a : A) (L1 L2 : list A),
 Disjoint L1 L2 → ¬ InEq a L2 → Disjoint (a :: L1) L2.
intros a L1 L2 H' H'0; apply DisjointCom; auto.
apply DisjointCons1; auto.
apply DisjointCom; auto.
Qed.

Theorem DisjointInclL :
 ∀ L1 L2 L3 : list A, Disjoint L1 L2 → InclEq L3 L1 → Disjoint L3 L2.
intros L1 L2 L3 H' H'0.
apply DisjointDef; auto.
intros a H'1; inversion H'.
apply H; auto.
inversion H'0; auto.
Qed.

Theorem DisjointInclR :
 ∀ L1 L2 L3 : list A, Disjoint L1 L2 → InclEq L3 L2 → Disjoint L1 L3.
intros L1 L2 L3 H' H'0.
apply DisjointCom.
apply DisjointInclL with (L1 := L2); auto.
apply DisjointCom; auto.
Qed.

Theorem DisjointIncl :
 ∀ L1 L2 L3 L4 : list A,
 Disjoint L1 L2 → InclEq L3 L1 → InclEq L4 L2 → Disjoint L3 L4.
intros L1 L2 L3 L4 H' H'0 H'1.
apply DisjointInclR with (L2 := L2); auto.
apply DisjointInclL with (L1 := L1); auto.
Qed.

Inductive append : list A → list A → list A → Prop :=
  | appendNil1 : ∀ L1 : list A, append L1 nil L1
  | appendNil2 : ∀ L2 : list A, append nil L2 L2
  | appendEqA :
      ∀ (a b : A) (L1 L2 L3 : list A),
      eqA a b → append L1 L2 L3 → append (a :: L1) (b :: L2) (a :: L3)
  | appendLtA1 :
      ∀ (a b : A) (L1 L2 L3 : list A),
      ltA a b →
      append L1 (b :: L2) L3 → append (a :: L1) (b :: L2) (a :: L3)
  | appendLtA2 :
      ∀ (a b : A) (L1 L2 L3 : list A),
      ltA b a →
      append (a :: L1) L2 L3 → append (a :: L1) (b :: L2) (b :: L3).
Hint Resolve appendNil1 appendNil2 appendEqA appendLtA1 appendLtA2.

Theorem appendCom :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 → Disjoint L1 L2 → append L2 L1 L3.
intros L1 L2 L3 H'; elim H'; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; inversion_clear H'3.
absurd (InEq a (b :: L5)); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3.
apply appendLtA2; auto.
apply H'2; auto.
apply DisjointInv2 with (a := a); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply appendLtA1; auto.
apply H'2; auto.
apply DisjointInv1 with (a := b); auto.
Qed.

Theorem appendIncl1 :
 ∀ L1 L2 L3 : list A, append L1 L2 L3 → InclEq L1 L3.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros a b L4 L5 L6 H'0 H'1 H'2.
apply InclEqDef; auto.
intros a0 H'3; inversion_clear H'3; auto.
inversion_clear H'2; auto.
intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto.
intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto.
intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto.
intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto.
Qed.

Theorem appendDisjIncl1 :
 ∀ L1 L2 L3 : list A, append L1 L2 L3 → Disjoint L1 L2 → incl L1 L3.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros L4 H'0; red in |- *; intros a H'1; inversion H'1.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; inversion_clear H'3.
lapply (H a); [ intros H'4; case H'4 | idtac ]; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_cons with (A := A);
 auto with datatypes; apply incl_tran with (m := L6);
 auto with datatypes.
apply H'2; apply DisjointInv2 with (a := a); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_tran with (m := L6);
 simpl in |- *; auto with datatypes.
apply H'2; apply DisjointInv1 with (a := b); auto.
Qed.

Theorem appendIncl2 :
 ∀ L1 L2 L3 : list A, append L1 L2 L3 → InclEq L2 L3.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef.
intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto.
apply InEqComp with (a := b); auto.
intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto.
intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto.
intros a b L4 L5 L6 H'0 H'1 H'2; apply InclEqDef; auto.
intros a0 H'3; inversion_clear H'2; inversion_clear H'3; auto.
Qed.

Theorem appendDisjIncl2 :
 ∀ L1 L2 L3 : list A, append L1 L2 L3 → Disjoint L1 L2 → incl L2 L3.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros L4 H'0; red in |- *; intros a H'1; inversion H'1.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; inversion_clear H'3.
lapply (H a); [ intros H'4; case H'4 | idtac ]; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_tran with (m := L6);
 auto with datatypes.
apply H'2; auto.
apply DisjointInv2 with (a := a); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3; apply incl_cons with (A := A);
 auto with datatypes; apply incl_tran with (m := L6);
 auto with datatypes.
apply H'2; apply DisjointInv1 with (a := b); auto.
Qed.

Theorem appendInv :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 → ∀ m : A, In m L3 → In m L1 ∨ In m L2.
intros L1 L2 L3 H'; elim H'; simpl in |- *; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elimc H'3; intros H'3;
 [ rewrite <- H'3 | idtac ]; auto.
elim (H'2 m); [ intros H'6 | intros H'6 | idtac ]; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elimc H'3; intros H'3; auto.
elim (H'2 m); [ intros H'6 | intros H'6 | idtac ]; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; Elimc H'3; intros H'3; auto.
elim (H'2 m); [ intros H'6 | intros H'6 | idtac ]; auto.
Qed.

Theorem appendEqInv :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 → ∀ m : A, InEq m L3 → InEq m L1 ∨ InEq m L2.
intros L1 L2 L3 H'; elim H'; simpl in |- *; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; inversion_clear H'3; auto.
case (H'2 m H); intros H'5; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; inversion_clear H'3; auto.
case (H'2 m H); intros H'5; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 m H'3; inversion_clear H'3; auto.
case (H'2 m H); intros H'5; auto.
Qed.

Theorem appendDisjoint :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 →
 ∀ L4 : list A, Disjoint L1 L4 → Disjoint L2 L4 → Disjoint L3 L4.
intros L1 L2 L3 H'; elim H'; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4.
apply DisjointCons2; auto.
apply H'2; auto.
apply DisjointInv2 with (a := a); auto.
apply DisjointInv2 with (a := b); auto.
inversion_clear H'3; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; apply DisjointCons2; auto.
apply H'2; auto.
apply DisjointInv2 with (a := a); auto.
inversion_clear H'3; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7 H'3 H'4; apply DisjointCons2; auto.
apply H'2; auto.
apply DisjointInv2 with (a := b); auto.
inversion_clear H'4; auto.
Qed.

Theorem appendSup :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 →
 ∀ a : A,
 (∀ b : A, In b L1 → ltA a b) →
 (∀ b : A, In b L2 → ltA a b) → ∀ b : A, In b L3 → ltA a b.
intros L1 L2 L3 H'; elim H'; simpl in |- *; auto;
 intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
 (Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]);
 auto.
Qed.

Theorem appendOlist :
 ∀ L1 L2 L3 : list A,
 append L1 L2 L3 → Olist L1 → Olist L2 → Olist L3.
intros L1 L2 L3 H'; elim H'; auto.
intros a b L4 L5 L6; case L6; auto.
intros a0 l H'0 H'1 H'2 H'3 H'4.
apply OlistCons; auto.
apply H'2; auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := b); auto.
apply appendSup with (L1 := L4) (L2 := L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := L4); auto.
intros b0 H'5.
apply ltAeqAComp with (a := b) (b := b0); auto.
apply OlistSup with (L := L5); auto.
simpl in |- *; auto.
intros a b L4 L5 L6; case L6; auto.
intros a0 l H'0 H'1 H'2 H'3 H'4.
apply OlistCons; auto.
apply H'2; auto.
apply OlistInv with (a := a); auto.
apply appendSup with (L1 := L4) (L2 := b :: L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := L4); auto.
intros b0 H'5.
apply OlistSup with (L := b :: L5); auto.
simpl in |- *; auto.
intros a b L4 L5 L6; case L6; auto.
intros a0 l H'0 H'1 H'2 H'3 H'4.
apply OlistCons; auto.
apply H'2; auto.
apply OlistInv with (a := b); auto.
apply appendSup with (L1 := a :: L4) (L2 := L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := a :: L4); auto.
intros b0 H'5.
apply OlistSup with (L := L5); auto.
simpl in |- *; auto.
Qed.


Definition appendf :=
  (fix aux1 (l1 l2 : list A) {struct l1} : list A :=
     match l1, l2 with
     | a :: t1, b :: t2 ⇒
         match ltADec a b with
         | inleft (left _) ⇒ a :: aux1 t1 (b :: t2)
         | inleft (right _) ⇒
             (fix aux2 (l3 : list A) : list A :=
                match l3 with
                | c :: t3 ⇒
                    match ltADec a c with
                    | inleft (left _) ⇒ a :: aux1 t1 (c :: t3)
                    | inleft (right _) ⇒ c :: aux2 t3
                    | inright _ ⇒ a :: aux1 t1 t3
                    end
                | nil ⇒ a :: t1
                end) (b :: t2)
         | inright _ ⇒ a :: aux1 t1 t2
         end
     | nil, _ ⇒ l2
     | _, nil ⇒ l1
     end).

Theorem appendfAppend : ∀ L1 L2 : list A, append L1 L2 (appendf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
apply appendLtA2; auto.
elim l0; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; auto.
Casec s1; intros s1; auto.
Qed.
Hint Resolve appendfAppend.

Theorem appendfIncl1 :
 ∀ L1 L2 : list A, Disjoint L1 L2 → incl L1 (appendf L1 L2).
intros L1 L2 HL1L2.
apply appendDisjIncl1 with (L2 := L2); auto.
Qed.

Theorem appendfIncl2 :
 ∀ L1 L2 : list A, Disjoint L1 L2 → incl L2 (appendf L1 L2).
intros L1 L2 HL1L2.
apply appendDisjIncl2 with (L1 := L1); auto.
Qed.

Theorem appendfInv :
 ∀ (L1 L2 : list A) (m : A), In m (appendf L1 L2) → In m L1 ∨ In m L2.
intros L1 L2 m H'.
apply appendInv with (L3 := appendf L1 L2); auto.
Qed.

Theorem appendfInclEq1 : ∀ L1 L2 : list A, InclEq L1 (appendf L1 L2).
intros L1 L2.
apply appendIncl1 with (L2 := L2); auto.
Qed.

Theorem appendfInclEq2 : ∀ L1 L2 : list A, InclEq L2 (appendf L1 L2).
intros L1 L2.
apply appendIncl2 with (L1 := L1); auto.
Qed.

Theorem appendfInvEq :
 ∀ (L1 L2 : list A) (m : A),
 InEq m (appendf L1 L2) → InEq m L1 ∨ InEq m L2.
intros L1 L2 m H'.
apply appendEqInv with (L3 := appendf L1 L2); auto.
Qed.

Theorem NotInAppendf :
 ∀ (L1 L2 : list A) (m : A),
 ¬ InEq m L1 → ¬ InEq m L2 → ¬ InEq m (appendf L1 L2).
intros L1 L2 m H' H'0; red in |- *; intros H'1.
case (appendfInvEq L1 L2 m H'1); auto.
Qed.

Theorem appendfDisjoint :
 ∀ L1 L2 : list A,
 Disjoint L1 L2 →
 ∀ L3 : list A,
 Disjoint L1 L3 → Disjoint L2 L3 → Disjoint (appendf L1 L2) L3.
intros L1 L2 HL1L2 L3 H' H'0.
apply appendDisjoint with (L1 := L1) (L2 := L2); auto.
Qed.

Theorem appendfOlist :
 ∀ L1 L2 : list A, Olist L1 → Olist L2 → Olist (appendf L1 L2).
intros L1 L2 H' H'0.
apply appendOlist with (L1 := L1) (L2 := L2); auto.
Qed.

Theorem Olistf : ∀ L : list A, Olist L → Olist (map f L).
intros L H'; elim H'; simpl in |- *; auto.
intros a b L0 H'0 H'1 H'2.
apply OlistCons; auto.
apply ltAeqAComp with (a := a) (b := b); auto.
Qed.

Theorem Disjointf :
 ∀ L1 L2 : list A, Disjoint L1 L2 → Disjoint L1 (map f L2).
intros L1 L2 H'; elim H'; auto.
intros L3 L4; elim L4; simpl in |- *; auto.
intros H'0.
apply DisjointDef; simpl in |- *; auto.
intros a l H'0 H'1.
apply DisjointCons1; auto.
apply H'0; auto.
intros a0 H'2; red in |- *; intros H'3.
lapply (H'1 a0); [ intros H'5; case H'5 | idtac ]; auto.
red in |- *; intros H'2.
lapply (H'1 (f a)); [ intros H'5; case H'5 | idtac ]; auto.
Qed.


Definition fappendf :=
  (fix aux1 (l1 l2 : list A) {struct l1} : list A :=
     match l1, l2 with
     | a :: t1, b :: t2 ⇒
         match ltADec a b with
         | inleft (left _) ⇒ a :: aux1 t1 (b :: t2)
         | inleft (right _) ⇒
             (fix aux2 (l3 : list A) : list A :=
                match l3 with
                | c :: t3 ⇒
                    match ltADec a c with
                    | inleft (left _) ⇒ a :: aux1 t1 (c :: t3)
                    | inleft (right _) ⇒ f c :: aux2 t3
                    | inright _ ⇒ a :: aux1 t1 t3
                    end
                | nil ⇒ a :: t1
                end) (b :: t2)
         | inright _ ⇒ a :: aux1 t1 t2
         end
     | nil, _ ⇒ map f l2
     | _, nil ⇒ l1
     end).

Theorem fappendfAppend :
 ∀ L1 L2 : list A, append L1 (map f L2) (fappendf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
apply appendLtA1; auto.
apply ltAeqAComp with (a := a) (b := a0); auto.
generalize (H' (a0 :: l0)); simpl in |- *; auto.
apply appendLtA2; auto.
apply ltAeqAComp with (a := a0) (b := a); auto.
elim l0; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; auto.
Casec s1; intros s1; auto.
simpl in |- ×.
apply appendLtA1; auto.
apply ltAeqAComp with (a := a) (b := a1); auto.
generalize (H' (a1 :: l1)); simpl in |- *; auto.
simpl in |- *; auto.
apply appendLtA2; auto.
apply ltAeqAComp with (a := a1) (b := a); auto.
simpl in |- ×.
apply appendEqA; auto.
apply eqATrans with a1; auto.
apply appendEqA; auto.
apply eqATrans with a0; auto.
Qed.
Hint Resolve fappendfAppend.

Theorem fappendfIncl1 :
 ∀ (L1 L2 : list A) (HL1L2 : Disjoint L1 L2), incl L1 (fappendf L1 L2).
intros L1 L2 HL1L2.
apply appendDisjIncl1 with (L2 := map f L2); auto.
apply Disjointf; auto.
Qed.

Theorem fappendfIncl2 :
 ∀ (L1 L2 : list A) (HL1L2 : Disjoint L1 L2),
 incl (map f L2) (fappendf L1 L2).
intros L1 L2 HL1L2.
apply appendDisjIncl2 with (L1 := L1); auto.
apply Disjointf; auto.
Qed.

Theorem fappendfInv :
 ∀ (L1 L2 : list A) (m : A),
 In m (fappendf L1 L2) → In m L1 ∨ In m (map f L2).
intros L1 L2 m H'.
apply appendInv with (L3 := fappendf L1 L2); auto.
Qed.

Theorem fappendfInclEq1 : ∀ L1 L2 : list A, InclEq L1 (fappendf L1 L2).
intros L1 L2.
apply appendIncl1 with (L2 := map f L2); auto.
Qed.

Theorem fappendfInclEq2 :
 ∀ L1 L2 : list A, InclEq (map f L2) (fappendf L1 L2).
intros L1 L2.
apply appendIncl2 with (L1 := L1); auto.
Qed.

Theorem fappendfInvEq :
 ∀ (L1 L2 : list A) (m : A),
 InEq m (fappendf L1 L2) → InEq m L1 ∨ InEq m (map f L2).
intros L1 L2 m H'.
apply appendEqInv with (L3 := fappendf L1 L2); auto.
Qed.

Theorem fappendfDisjoint :
 ∀ (L1 L2 : list A) (HL1L2 : Disjoint L1 L2) (L3 : list A),
 Disjoint L1 L3 → Disjoint L2 L3 → Disjoint (fappendf L1 L2) L3.
intros L1 L2 HL1L2 L3 H' H'0.
apply appendDisjoint with (L1 := L1) (L2 := map f L2); auto.
apply DisjointCom.
apply Disjointf.
apply DisjointCom; auto.
Qed.

Theorem fappendfOlist :
 ∀ L1 L2 : list A, Olist L1 → Olist L2 → Olist (fappendf L1 L2).
intros L1 L2 H' H'0.
apply appendOlist with (L1 := L1) (L2 := map f L2); auto.
apply Olistf; auto.
Qed.

Variable test : A → A → Prop.
Variable testDec : ∀ a b : A, eqA a b → {test a b} + {¬ test a b}.
Variable testEq : ∀ a b : A, test a b → eqA a b.


Definition getMin :=
  (fix aux1 (l1 l2 : list A) {struct l1} : Option A :=
     match l1, l2 with
     | a :: t1, b :: t2 ⇒
         match ltADec a b with
         | inleft (left _) ⇒ aux1 t1 (b :: t2)
         | inleft (right _) ⇒
             (fix aux2 (l3 : list A) : Option A :=
                match l3 with
                | c :: t3 ⇒
                    match ltADec a c with
                    | inleft (left _) ⇒ aux1 t1 (c :: t3)
                    | inleft (right _) ⇒ aux2 t3
                    | inright H ⇒
                        match testDec a c H with
                        | left _ ⇒ Some A a
                        | right __ ⇒ aux2 t3
                        end
                    end
                | nil ⇒ None A
                end) (b :: t2)
         | inright H ⇒
             match testDec a b H with
             | left _ ⇒ Some A a
             | right _ ⇒ aux1 t1 t2
             end
         end
     | nil, _ ⇒ None A
     | _, nil ⇒ None A
     end).

Theorem geMinIn :
 ∀ (L1 L2 : list A) (a : A),
 Olist L1 → Olist L2 → getMin L1 L2 = Some _ a → In a L1.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a H' H'0 H'1; discriminate.
intros a l a0 H' H'0 H'1; discriminate.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 H'0 H'1 H'2; discriminate.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2; right.
apply (H' (a0 :: l0)); auto.
apply OlistInv with (a := a); auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4; right.
apply (H' (a2 :: l1)); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros H'4; case H'2; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
intros H'4 H'5; case H'2; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3; auto.
intros H'2 H'3; right.
apply (H' l0); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
Qed.

Theorem getMinComp :
 ∀ (L1 L2 : list A) (a : A),
 Olist L1 →
 Olist L2 → getMin L1 L2 = Some _ a → ∃ b : A, test a b ∧ In b L2.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a H' H'0 H'1; discriminate.
intros a l a0 H' H'0 H'1; discriminate.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 H'0 H'1 H'2; discriminate.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2; case (H' (a0 :: l0) a1); auto.
apply OlistInv with (a := a); auto.
intros x H'3; elim H'3; intros H'4 H'5; ∃ x; auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4; case (H' (a2 :: l1) a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros x H'5; elim H'5; intros H'6 H'7; ∃ x; auto.
intros H'4; case H'2; auto.
apply OlistSkip with (b := a2); auto.
intros x H'5; elim H'5; intros H'6 H'7; ∃ x; intuition.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
∃ a2; split; auto with datatypes.
rewrite <- H0; auto.
intros H'4 H'5; case H'2; auto.
apply OlistSkip with (b := a2); auto.
intros x H'6; elim H'6; intros H'7 H'8; ∃ x; split; auto with datatypes;
 case H'8; auto with datatypes.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3; auto.
∃ a0; split; auto with datatypes.
rewrite <- H0; auto.
intros H'2 H'3; case (H' l0 a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros x H'4; elim H'4; intros H'5 H'6; ∃ x; auto.
Qed.

Theorem getMinMin :
 ∀ (L1 L2 : list A) (a : A),
 Olist L1 →
 Olist L2 →
 getMin L1 L2 = Some _ a →
 ∀ b c : A, ltA b a → In b L1 → In c L2 → ¬ test b c.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0 a1 H'0 H'1.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'2 b c H'3 H'4 H'5; Casec H'4; intros H'4; auto.
rewrite <- H'4; auto.
red in |- *; intros H'6; absurd (In c (a0 :: l0)); auto.
apply OlistUnique with (a := a); auto.
apply (H' (a0 :: l0) a1); auto.
apply OlistInv with (a := a); auto.
generalize H'1; elim l0; auto.
intros H'2 H'3; discriminate.
intros a2 l1 H'2 H'3.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'4 b c H'5 H'6 H'7; Casec H'6; intros H'6; auto.
rewrite <- H'6; auto.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
red in |- *; intros H'8; absurd (eqA a0 a); auto.
red in |- *; intros H'8; absurd (In c (a2 :: l1)); auto.
apply OlistUnique with (a := a); auto.
apply OlistCons; auto.
apply OlistInv with (a := a0); auto.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
red in |- *; intros H'8; Contradict H'6; auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
apply (H' (a2 :: l1) a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
simpl in |- *; intros H'4 b c H'5 H'6 H'7; auto.
Casec H'7; intros H'7; auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto.
Casec H'7; intros H'7; auto.
rewrite <- H'7.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
red in |- *; intros H'8; absurd (eqA a2 a); auto.
Contradict H'6.
apply OlistUnique with (a := a2); auto.
apply OlistSkip with (b := a); auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'4); auto.
case (testDec a a2 s1); auto.
intros H'4 H'5; inversion H'5; auto.
rewrite <- H0.
intros b c H'6 H'7 H'8; absurd (In b (a :: l)); auto.
apply OlistUnique with (a := b); auto.
intros H'4 H'5 b c H'6 H'7 H'8.
Elimc H'8; simpl in |- *; intros H'8.
apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto.
Elimc H'8; simpl in |- *; intros H'8.
rewrite <- H'8.
Elimc H'7; intros H'7; [ rewrite <- H'7 | idtac ]; auto.
Contradict H'7; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a2; auto.
apply (H'2 (OlistSkip _ _ _ H'3) H'5); auto.
case (testDec a a0 s); auto.
intros H'2 H'3; inversion H'3.
intros b c H'4 H'5 H'6.
Elimc H'5; intros H'5; [ rewrite <- H'5 in H'4; Contradict H'4 | idtac ];
 auto.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
Contradict H'5.
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
Contradict H'5.
apply OlistUnique with (a := b); auto.
apply OlistSkip with (b := a1); auto.
apply OlistCons; auto.
rewrite <- H0; auto.
intros H'2 H'3 b c H'4 H'5 H'6.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ]; auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
Contradict H'5.
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
Contradict H'6.
apply OlistUnique with (a := a0); auto.
apply eqATrans with a; auto.
apply (H' l0 a1); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
Qed.

Theorem getMinNone :
 ∀ L1 L2 : list A,
 Olist L1 →
 Olist L2 →
 getMin L1 L2 = None _ → ∀ a b : A, In a L1 → In b L2 → ¬ test a b.
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; auto with datatypes.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
intros a0 l0 a1 H'0.
case (ltADec a a0); intros s; auto.
Casec s; intros s; auto.
intros H'1 a2 b H'2; Elimc H'2; intros H'2; [ rewrite <- H'2 | idtac ]; auto.
intros H'3; red in |- *; intros H'4; absurd (In b (a0 :: l0)); auto.
apply OlistUnique with (a := a); auto.
intros H'3; apply (H' (a0 :: l0)); auto.
apply OlistInv with (a := a); auto.
generalize H'0; elim l0; auto.
intros H'1 H'2 a2 b H'3 H'4; Elimc H'4; intros H'4;
 [ rewrite <- H'4 | idtac ]; auto.
Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ].
red in |- *; intros H'5; absurd (eqA a0 a); auto.
Contradict H'3; auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
intros a2 l1 H'1 H'2.
case (ltADec a a2); intros s1; auto.
Casec s1; intros s1; auto.
intros H'3 a3 b H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto.
intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
red in |- *; intros H'6; absurd (eqA a0 a); auto.
Contradict H'5; auto.
apply OlistUnique with (a := a); auto.
apply OlistCons; auto.
apply OlistInv with (a := a0); auto.
intros H'5; Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ].
Contradict H'4; auto.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
apply (H' (a2 :: l1)); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
intros H'3 a3 b H'4 H'5.
Elimc H'5; simpl in |- *; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ].
red in |- *; intros H'6; absurd (eqA a2 a); auto.
Contradict H'4.
apply OlistUnique with (a := a2); auto.
apply OlistSkip with (b := a); auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a2 s1); auto.
intros H'3 H'4; discriminate.
intros H'3 H'4 a3 b H'5 H'6.
Elimc H'6; simpl in |- *; intros H'6; [ rewrite <- H'6 | idtac ].
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ].
red in |- *; intros H'7; absurd (eqA a0 a); auto.
Contradict H'5.
apply OlistUnique with (a := a0); auto.
apply OlistSkip with (b := a); auto.
Elimc H'6; intros H'6; [ rewrite <- H'6 | idtac ].
Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]; auto.
Contradict H'5.
apply OlistUnique with (a := a); auto.
apply eqATrans with a2; auto.
apply H'1; auto.
apply OlistSkip with (b := a2); auto.
case (testDec a a0 s); auto.
intros H'1 H'2; discriminate.
intros H'1 H'2 a2 b H'3; Elimc H'3; intros H'3; [ rewrite <- H'3 | idtac ];
 auto.
intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ]; auto.
Contradict H'4; auto.
apply OlistUnique with (a := a0); auto.
apply eqATrans with a; auto.
intros H'4; Elimc H'4; intros H'4; [ rewrite <- H'4 | idtac ].
Contradict H'3; auto.
apply OlistUnique with (a := a); auto.
apply eqATrans with a0; auto.
apply (H' l0); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
Qed.

Inductive inter : list A → list A → list A → Prop :=
  | interNil1 : ∀ L1 : list A, inter L1 nil nil
  | interNil2 : ∀ L2 : list A, inter nil L2 nil
  | interEqA :
      ∀ (a b : A) (L1 L2 L3 : list A),
      eqA a b → inter L1 L2 L3 → inter (a :: L1) (b :: L2) (a :: L3)
  | interLtA1 :
      ∀ (a b : A) (L1 L2 L3 : list A),
      ltA a b → inter L1 (b :: L2) L3 → inter (a :: L1) (b :: L2) L3
  | interLtA2 :
      ∀ (a b : A) (L1 L2 L3 : list A),
      ltA b a → inter (a :: L1) L2 L3 → inter (a :: L1) (b :: L2) L3.

Theorem interIncl1 : ∀ L1 L2 L3 : list A, inter L1 L2 L3 → InclEq L3 L1.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros a b L4 L5 L6 H'0 H'1 H'2.
apply InclEqCons; auto.
apply InclEqTrans with (y := L4); auto.
intros a b L4 L5 L6 H'0 H'1 H'2.
apply InclEqTrans with (y := L4); auto.
Qed.

Theorem interIncl2 : ∀ L1 L2 L3 : list A, inter L1 L2 L3 → InclEq L3 L2.
intros L1 L2 L3 H'; elim H'; auto with datatypes.
intros a b L4 L5 L6 H'0 H'1 H'2.
apply InclEqCons; auto.
apply InclEqTrans with (y := L5); auto.
intros a b L4 L5 L6 H'0 H'1 H'2.
apply InclEqTrans with (y := L5); auto.
Qed.

Theorem interSup :
 ∀ L1 L2 L3 : list A,
 inter L1 L2 L3 →
 ∀ a : A,
 (∀ b : A, In b L1 → ltA a b) →
 (∀ b : A, In b L2 → ltA a b) → ∀ b : A, In b L3 → ltA a b.
intros L1 L2 L3 H'; elim H'; simpl in |- *; auto;
 intros a b L4 L5 L6 H'0 H'1 H'2 a0 H'3 H'4 b0 H'5;
 (Elimc H'5; intros H'5; [ rewrite <- H'5 | idtac ]);
 auto.
Qed.

Theorem interOlist :
 ∀ L1 L2 L3 : list A, inter L1 L2 L3 → Olist L1 → Olist L2 → Olist L3.
intros L1 L2 L3 H'; elim H'; auto.
intros a b L4 L5 L6; case L6; auto.
intros a0 l H'0 H'1 H'2 H'3 H'4.
apply OlistCons; auto.
apply H'2; auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := b); auto.
apply interSup with (L1 := L4) (L2 := L5) (L3 := a0 :: l); auto.
intros b0 H'5.
apply OlistSup with (L := L4); auto.
intros b0 H'5.
apply ltAeqAComp with (a := b) (b := b0); auto.
apply OlistSup with (L := L5); auto.
simpl in |- *; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3 H'4.
apply H'2; auto.
apply OlistInv with (a := a); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 H'3 H'4.
apply H'2; auto.
apply OlistInv with (a := b); auto.
Qed.

Theorem InEqNList : ∀ (a : A) (L : list A), InEq a L → ¬ Olist (a :: L).
intros a L; elim L; auto.
intros H'; inversion H'; auto.
intros a0 l H' H'0; inversion H'0; auto.
red in |- *; intros H'1; inversion H'1; auto.
absurd (eqA a a0); auto.
red in |- *; intros H'1; case H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem InEqSup :
 ∀ (a b : A) (L : list A), InEq a L → Olist (b :: L) → ltA b a.
intros a b L; elim L; auto.
intros H'; inversion H'; auto.
intros a0 l H' H'0 H'1; inversion H'0; auto.
apply ltAeqAComp with (a := b) (b := a0); auto.
apply OlistSup with (L := a0 :: l); auto with datatypes.
apply H'; auto.
apply OlistSkip with (b := a0); auto.
Qed.

Theorem InEqOlistInv :
 ∀ (a b : A) (L1 L2 : list A),
 InclEq (a :: L1) (b :: L2) →
 Olist (a :: L1) →
 Olist (b :: L2) → InclEq (a :: L1) L2 ∨ eqA a b ∧ InclEq L1 L2.
intros a b L1 L2 H' H'0 H'1.
case (ltADec a b); intros Eqab.
Casec Eqab; intros Eqab.
absurd (Olist (a :: b :: L2)); auto.
apply InEqNList; auto.
inversion H'; auto.
left.
inversion H'; auto.
apply InclEqDef; auto.
intros a0 H'2.
lapply (H a0); [ intros H'4 | idtac ]; auto.
inversion H'4; auto.
absurd (Olist (a0 :: a :: L1)); auto.
apply InEqNList; auto.
apply OlistCons; auto.
apply ltAeqAComp with (a := b) (b := a); auto.
right; split; auto.
apply InclEqDef; auto.
intros a0 H'2.
inversion H'.
lapply (H a0); [ intros H'4 | idtac ]; auto.
inversion H'4; auto.
absurd (eqA a a0); auto.
apply ltAImpNotEqA; auto.
apply InEqSup with (L := L1); auto.
apply eqATrans with (y := b); auto.
Qed.

Theorem interMin :
 ∀ L1 L2 L3 L4 : list A,
 inter L1 L2 L3 →
 Olist L1 →
 Olist L2 →
 Olist L3 → Olist L4 → InclEq L4 L1 → InclEq L4 L2 → InclEq L4 L3.
intros L1 L2 L3 L4 H'; generalize L4; clear L4; elim H'; auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7; case L7; auto.
intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
case (eqADec a0 a); auto.
intros H'9.
apply InclEqCons; auto.
apply InclEqTrans with (y := L6); auto.
apply H'2; auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := b); auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := a0); auto.
apply InclEqOlist with (a := a0) (b := a); auto.
apply InclEqOlist with (a := a0) (b := b); auto.
intros H'9.
apply InclEqTrans with (y := L6); auto.
apply H'2; auto.
apply OlistInv with (a := a); auto.
apply OlistInv with (a := b); auto.
apply OlistInv with (a := a); auto.
elim (InEqOlistInv a0 a l L4);
 [ intros H'17; apply H'17
 | intros H'17; elim H'17; intros H'18
 | idtac
 | idtac
 | idtac ]; auto.
case H'9; auto.
elim (InEqOlistInv a0 b l L5);
 [ intros H'17; apply H'17
 | intros H'17; elim H'17; intros H'18
 | idtac
 | idtac
 | idtac ]; auto.
case H'9; auto.
apply eqATrans with (y := b); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7; case L7; auto.
intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
apply H'2; auto.
apply OlistInv with (a := a); auto.
elim (InEqOlistInv a0 a l L4);
 [ intros H'17; apply H'17
 | intros H'17; elim H'17; intros H'18
 | idtac
 | idtac
 | idtac ]; auto.
absurd (Olist (a0 :: b :: L5)); auto.
apply InEqNList; auto.
inversion H'8; auto.
apply OlistCons; auto.
apply ltAeqAComp with (a := a) (b := b); auto.
intros a b L4 L5 L6 H'0 H'1 H'2 L7; case L7; auto.
intros a0 l H'3 H'4 H'5 H'6 H'7 H'8.
apply H'2; auto.
apply OlistInv with (a := b); auto.
elim (InEqOlistInv a0 b l L5);
 [ intros H'17; apply H'17
 | intros H'17; elim H'17; intros H'18
 | idtac
 | idtac
 | idtac ]; auto.
absurd (Olist (a0 :: a :: L4)); auto.
apply InEqNList; auto.
inversion H'7; auto.
apply OlistCons; auto.
apply ltAeqAComp with (a := b) (b := a); auto.
Qed.

Theorem interCom :
 ∀ L1 L2 L3 L4 : list A,
 inter L1 L2 L3 →
 inter L2 L1 L4 → Olist L1 → Olist L2 → Olist L3 → Olist L4 → EqL L3 L4.
intros L1 L2 L3 L4 H' H'0 H'1 H'2 H'3 H'4.
apply EqLOlist; auto.
apply interMin with (L1 := L2) (L2 := L1); auto.
apply interIncl2 with (L1 := L1); auto.
apply interIncl1 with (L2 := L2); auto.
apply interMin with (L1 := L1) (L2 := L2); auto.
apply interIncl2 with (L1 := L2); auto.
apply interIncl1 with (L2 := L1); auto.
Qed.


Definition interf :=
  (fix aux1 (l1 l2 : list A) {struct l1} : list A :=
     match l1, l2 with
     | a :: t1, b :: t2 ⇒
         match ltADec a b with
         | inleft (left _) ⇒ aux1 t1 (b :: t2)
         | inleft (right _) ⇒
             (fix aux2 (l3 : list A) : list A :=
                match l3 with
                | c :: t3 ⇒
                    match ltADec a c with
                    | inleft (left _) ⇒ aux1 t1 (c :: t3)
                    | inleft (right _) ⇒ aux2 t3
                    | inright _ ⇒ a :: aux1 t1 t3
                    end
                | nil ⇒ nil
                end) (b :: t2)
         | inright _ ⇒ a :: aux1 t1 t2
         end
     | nil, _ ⇒ nil
     | _, nil ⇒ nil
     end).

Theorem interfProp1 : ∀ L1 L2 : list A, inter L1 L2 (interf L1 L2).
intros L1; elim L1; simpl in |- ×.
intros L2; case L2; simpl in |- *; intros; apply interNil2; auto.
intros a l H' L2; case L2; simpl in |- *; auto with datatypes.
apply interNil1; auto.
intros a0 l0.
case (ltADec a a0); intros s; [ Casec s; intros s | idtac ].
apply interLtA1; auto.
apply interLtA2; auto.
elim l0; auto.
apply interNil1; auto.
intros a1 l1 H'0.
case (ltADec a a1); intros s1; [ Casec s1; intros s1 | idtac ].
apply interLtA1; auto.
apply interLtA2; auto.
apply interEqA; auto.
apply interEqA; auto.
Qed.
Hint Resolve interfProp1.

Theorem interfIncl1 : ∀ L1 L2 : list A, InclEq (interf L1 L2) L1.
intros L1 L2.
apply interIncl1 with (L2 := L2); auto.
Qed.

Theorem interfIncl2 : ∀ L1 L2 : list A, InclEq (interf L1 L2) L2.
intros L1 L2.
apply interIncl2 with (L1 := L1); auto.
Qed.

Theorem interfOlist :
 ∀ L1 L2 : list A, Olist L1 → Olist L2 → Olist (interf L1 L2).
intros L1 L2 H' H'0.
apply interOlist with (L1 := L1) (L2 := L2); auto.
Qed.

Theorem interfMin :
 ∀ L1 L2 L3 : list A,
 Olist L1 →
 Olist L2 →
 Olist L3 → InclEq L3 L1 → InclEq L3 L2 → InclEq L3 (interf L1 L2).
intros L1 L2 L3 H' H'0 H'1 H'2 H'3.
apply interMin with (L1 := L1) (L2 := L2); auto.
apply interfOlist; auto.
Qed.

Theorem interfCom :
 ∀ L1 L2 : list A,
 Olist L1 → Olist L2 → EqL (interf L1 L2) (interf L2 L1).
intros L1 L2 H' H'0.
apply interCom with (L1 := L1) (L2 := L2); auto.
apply interfOlist; auto.
apply interfOlist; auto.
Qed.
End OrderedList.