Require Export MSets.
Require Import Arith.
Require Import NArith.
Require Import Notations.
Require Import Sorting.
Require Import Coq.Program.Equality.
Require Export GeoCoq.Tactics.Coinc.tactics_axioms.

Module S := MSetList.Make PositiveOrderedTypeBits.
(*
We choose to use lists as it is as fast as AVLs for a limited number of points but they are easier to debug.
Module S := MSetAVL.Make PositiveOrderedTypeBits.
*)

Module SWP := WPropertiesOn PositiveOrderedTypeBits S.

Module SetOfSetsOfPositiveOrderedType <: OrderedType.

  Definition t := S.t.

  Definition eq := S.Equal.

  Include IsEq.

  Definition eqb := S.equal.

  Definition eqb_eq := S.equal_spec.

  Include HasEqBool2Dec.

  Definition lt := S.lt.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.
  Proof.
(* Goal: @Proper (forall (_ : S.t) (_ : S.t), Prop) (@respectful S.t (forall _ : S.t, Prop) eq (@respectful S.t Prop eq iff)) lt *)
  apply S.lt_compat.
 Qed.

  Instance lt_strorder : StrictOrder lt.
  Proof.
(* Goal: @StrictOrder S.t lt *)
  apply S.lt_strorder.
 Qed.

  Definition compare := S.compare.

  Definition compare_spec := S.compare_spec.

End SetOfSetsOfPositiveOrderedType.

Module SS := MSetList.Make SetOfSetsOfPositiveOrderedType.
(*
Module SS := MSetAVL.Make SetOfSetsOfPositiveOrderedType.
*)

Definition fstpp (pair : (positive * positive)) :=
  match pair with
    |(a,b) => Pos.min a b
  end.

Definition sndpp (pair : (positive * positive)) :=
  match pair with
    |(a,b) => Pos.max a b
  end.

Module SetOfPairsOfPositiveOrderedType <: OrderedType.

  Definition t:= (positive * positive).

  Definition eq (t1 t2 : t) :=
    Pos.eq (fstpp(t1)) (fstpp(t2)) /\ Pos.eq (sndpp(t1)) (sndpp(t2)).

  Include IsEq.

  Definition eqb (t1 t2 : t) :=
    Pos.eqb (fstpp(t1)) (fstpp(t2)) && Pos.eqb (sndpp(t1)) (sndpp(t2)).

  Lemma eqb_eq : forall t1 t2, eqb t1 t2 = true <-> eq t1 t2.
  Proof.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
  intros.
(* Goal: iff (@Logic.eq bool (eqb t1 t2) true) (eq t1 t2) *)
  unfold eqb; unfold eq.
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
  split; intro H.

(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
    apply andb_true_iff in H.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) (compareList l1 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
    induction H.
(* Goal: and (@Logic.eq bool (Pos.eqb (fstpp t1) (fstpp t2)) true) (@Logic.eq bool (Pos.eqb (sndpp t1) (sndpp t2)) true) *)
    split; apply Pos.eqb_eq; assumption.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) (compareList l1 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
    induction H.
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
    apply andb_true_iff.
(* Goal: and (@Logic.eq bool (Pos.eqb (fstpp t1) (fstpp t2)) true) (@Logic.eq bool (Pos.eqb (sndpp t1) (sndpp t2)) true) *)
    split; apply Pos.eqb_eq; assumption.
 Qed.

  Include HasEqBool2Dec.

  Definition lt (t1 t2 : t) :=
    let ft1 := fstpp(t1) in
    let ft2 := fstpp(t2) in
    let st1 := sndpp(t1) in
    let st2 := sndpp(t2) in
    if Pos.eqb ft1 ft2 then Pos.lt st1 st2
                       else Pos.lt ft1 ft2.

  Lemma lt_irrefl : Irreflexive lt.
  Proof.
  assert (HIP : Irreflexive Pos.lt)
    by (apply StrictOrder_Irreflexive; assumption).
(* Goal: forall x : t, not (lt x x) *)
  unfold Irreflexive in *.
(* Goal: forall x : t, not (lt x x) *)
  unfold Reflexive in *.
(* Goal: forall x : t, not (lt x x) *)
  unfold complement in *.
(* Goal: forall (x : t) (_ : lt x x), False *)
  intro x.
(* Goal: @Transitive tST ltST *)
  unfold lt.
  assert (HEq : Pos.eqb (fstpp(x)) (fstpp(x)) = true)
    by (apply Pos.eqb_eq; intuition).
(* Goal: forall _ : if Pos.eqb (fstpp x) (fstpp x) then Pos.lt (sndpp x) (sndpp x) else Pos.lt (fstpp x) (fstpp x), False *)
  rewrite HEq.
(* Goal: forall _ : Pos.lt (sndpp x) (sndpp x), False *)
  apply HIP.
 Qed.

  Lemma lt_antiref : forall x, ~ lt x x.
  Proof.
(* Goal: forall x : t, not (lt x x) *)
  assert (HIL : Irreflexive lt) by (apply lt_irrefl).
(* Goal: forall x : t, not (lt x x) *)
  unfold Irreflexive in *.
(* Goal: forall x : t, not (lt x x) *)
  unfold Reflexive in *.
(* Goal: forall x : t, not (lt x x) *)
  unfold complement in *.
(* Goal: forall x : t, not (lt x x) *)
  intros x H.
(* Goal: False *)
  apply HIL with x.
(* Goal: False *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
  apply H.
 Qed.

  Lemma lt_trans : Transitive lt.
  Proof.
(* Goal: @Transitive t lt *)
  assert (HTP : Transitive Pos.lt) by (apply StrictOrder_Transitive; assumption).
(* Goal: @Transitive t lt *)
  unfold Transitive in *.
(* Goal: forall (x y z : t) (_ : lt x y) (_ : lt y z), lt x z *)
  intros x y z.
(* Goal: @Transitive tST ltST *)
  unfold lt.
(* Goal: forall (_ : if Pos.eqb (fstpp x) (fstpp y) then Pos.lt (sndpp x) (sndpp y) else Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
  case_eq (Pos.eqb (fstpp(x)) (fstpp(y))).

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) true) (_ : Pos.lt (sndpp x) (sndpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
    intro HEqXY.
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
    case_eq (Pos.eqb (fstpp(y)) (fstpp(z))).

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) true) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      intro HEqYZ.
      assert (HEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = true)
        by (apply Pos.eqb_eq in HEqXY; rewrite HEqXY; assumption).
(* Goal: forall (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      rewrite HEqXZ.
(* Goal: forall (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      apply HTP.

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      intro HNEqYZ.
      assert (HNEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = false)
        by (apply Pos.eqb_eq in HEqXY; rewrite HEqXY; assumption).
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      rewrite HNEqXZ.
(* Goal: forall (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      apply Pos.eqb_eq in HEqXY; rewrite HEqXY.
(* Goal: forall (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp y) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      intro.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      intuition.

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
    intro HNEqXY.
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
    case_eq (Pos.eqb (fstpp(y)) (fstpp(z))).

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) true) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      intro HEqYZ.
      assert (HNEqXZ : Pos.eqb (fstpp(x)) (fstpp(z)) = false)
        by (apply Pos.eqb_eq in HEqYZ; rewrite <- HEqYZ; assumption).
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      rewrite HNEqXZ.
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (sndpp y) (sndpp z)), Pos.lt (fstpp x) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      apply Pos.eqb_eq in HEqYZ; rewrite HEqYZ.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
      intros.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      assumption.

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp y) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      intro HNEqYZ.
(* Goal: forall (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
      case_eq (Pos.eqb (fstpp(x)) (fstpp(z))).

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) true) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        intro HEqXZ.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
        intros.
        assert (HLtXZ : Pos.ltb (fstpp(x)) (fstpp(z)) = true)
          by (apply Pos.ltb_lt; apply HTP with (fstpp(y)); assumption).
(* Goal: Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        apply Pos.eqb_eq in HEqXZ; rewrite HEqXZ in HLtXZ.
        assert (HIP : Irreflexive Pos.lt)
          by (apply StrictOrder_Irreflexive; assumption).
(* Goal: Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        unfold Irreflexive in HIP.
(* Goal: Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        unfold Reflexive in HIP.
(* Goal: Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        unfold complement in HIP.
(* Goal: Pos.lt (sndpp x) (sndpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        exfalso.
(* Goal: False *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        apply HIP with (fstpp(z)).
(* Goal: Pos.lt (fstpp z) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        apply Pos.ltb_lt in HLtXZ.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp z)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp x) (fstpp z) *)
        intro HNEqXZ.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
        intros.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply HTP with (fstpp(y)); assumption.
 Qed.

  Instance lt_compat : Proper (eq==>eq==>iff) lt.
  Proof.
  intros x y HXY x' y' HX'Y'.
  unfold lt; unfold eq in *.
  elim HXY; intros HXYF HXYS.
  elim HX'Y'; intros HX'Y'F HX'Y'S.
  clear HXY; clear HX'Y'.
  unfold Pos.eq in *.
  case_eq (Pos.eqb (fstpp(x)) (fstpp(x'))); intro HXX'F.

    assert (HYY'F : Pos.eqb (fstpp(y)) (fstpp(y')) = true).
    apply Pos.eqb_eq in HXX'F.
    apply Pos.eqb_eq.
    rewrite <- HXYF.
    rewrite <- HX'Y'F.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    assumption.

    rewrite HYY'F.
    case_eq (Pos.eqb (sndpp(x)) (sndpp(x'))); intro HXX'S.

      apply Pos.eqb_eq in HXX'S.
      assert (HYY'S : Pos.eqb (sndpp(y)) (sndpp(y')) = true).
      apply Pos.eqb_eq.
      rewrite <- HXYS.
      rewrite <- HX'Y'S.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      assumption.

      apply Pos.eqb_eq in HYY'S.
      rewrite HYY'S.
      rewrite HXX'S.
      rewrite HX'Y'S.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      intuition.

      rewrite HXYS.
      rewrite HX'Y'S.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      intuition.

    assert (HYY'F : Pos.eqb (fstpp(y)) (fstpp(y')) = false).
    rewrite <- HXYF.
    rewrite <- HX'Y'F.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    assumption.

    rewrite HYY'F.
    rewrite HXYF.
    rewrite HX'Y'F.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
    intuition.
 Qed.

  Instance lt_strorder : StrictOrder lt.
  Proof.
  apply Build_StrictOrder.
  apply lt_irrefl.
  apply lt_trans.
 Qed.

  Definition compare t1 t2 :=
    let ft1 := fstpp(t1) in
    let ft2 := fstpp(t2) in
    let st1 := sndpp(t1) in
    let st2 := sndpp(t2) in
    match (Pos.compare ft1 ft2) with
      | Lt => Lt
      | Eq => Pos.compare st1 st2
      | Gt => Gt
    end.

  Lemma compare_spec : forall t1 t2, CompSpec eq lt t1 t2 (compare t1 t2).
  Proof.
(* Goal: forall t1 t2 : t, @CompSpec t eq lt t1 t2 (compare t1 t2) *)
  intros t1 t2.
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
  case_eq (Pos.eqb (fstpp(t1)) (fstpp(t2))); intro HF.

(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
    apply Pos.eqb_eq in HF.
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
    case_eq (Pos.eqb (sndpp(t1)) (sndpp(t2))); intro HS.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      apply Pos.eqb_eq in HS.
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      unfold CompSpec.

(* Goal: CompareSpec (eq t1 t2) (lt t1 t2) (lt t2 t1) (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      assert (HC : compare t1 t2 = Eq).
(* Goal: @Logic.eq comparison (compare t1 t2) Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      unfold compare.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      unfold Pos.compare.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
      rewrite HF.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t2) (fstpp t2)) Eq *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      apply Pos.compare_cont_refl.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Eq *)
(* Goal: CompareSpec (eq t1 t2) (lt t1 t2) (lt t2 t1) (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Eq).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      unfold Pos.compare.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (sndpp t1) (sndpp t2)) Eq *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Eq *)
(* Goal: CompareSpec (eq t1 t2) (lt t1 t2) (lt t2 t1) (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      rewrite HS.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t2) (fstpp t2)) Eq *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      apply Pos.compare_cont_refl.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      rewrite HCF; rewrite HCS.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      rewrite HC.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Eq *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Gt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
      apply CompEq.
(* Goal: eq t1 t2 *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      unfold eq.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      rewrite HF; rewrite HS; split; intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      case_eq (Pos.ltb (sndpp(t1)) (sndpp(t2))); intro HLS.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HC : compare t1 t2 = Lt).
(* Goal: @Logic.eq comparison (compare t1 t2) Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold compare.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t2) (fstpp t2)) Eq *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.compare_cont_refl.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Lt).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: Pos.lt (sndpp t1) (sndpp t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLS.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t1) (fstpp t2)) Lt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.nat_of_P_lt_Lt_compare_complement_morphism.
(* Goal: Peano.lt (Pos.to_nat (fstpp t1)) (Pos.to_nat (fstpp t2)) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.Pos2Nat.inj_lt.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HCF; rewrite HCS.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HC.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        apply CompLt.
(* Goal: @Transitive tST ltST *)
        unfold lt.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.eqb_eq in HF.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: Pos.lt (sndpp t1) (sndpp t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLS.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HLS2 : Pos.ltb (sndpp(t2)) (sndpp(t1)) = true).
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_nlt in HLS.
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.le_nlt in HLS.
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.lt_eq_cases in HLS.
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        elim HLS; intro HLS2.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.eqb_neq in HS.
(* Goal: @Logic.eq bool (Pos.ltb (sndpp t2) (sndpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HLS2 in HS.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HC : compare t1 t2 = Gt).
(* Goal: @Logic.eq comparison (compare t1 t2) Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold compare.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Eq).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t2) (fstpp t2)) Eq *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.compare_cont_refl.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCS : Pos.compare (sndpp(t1)) (sndpp(t2)) = Gt).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: Pos.lt (sndpp t2) (sndpp t1) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLS2.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.nat_of_P_gt_Gt_compare_complement_morphism.
(* Goal: gt (Pos.to_nat (fstpp t1)) (Pos.to_nat (fstpp t2)) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.Pos2Nat.inj_gt.
(* Goal: Pos.gt (fstpp t1) (fstpp t2) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.gt_lt_iff.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HCF; rewrite HCS.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HC.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Gt *)
        apply CompGt.
(* Goal: @Transitive tST ltST *)
        unfold lt.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.eqb_eq in HF.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite Pos.eqb_sym in HF.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: Pos.lt (sndpp t2) (sndpp t1) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLS2.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
      case_eq (Pos.ltb (fstpp(t1)) (fstpp(t2))); intro HLF.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HC : compare t1 t2 = Lt).
(* Goal: @Logic.eq comparison (compare t1 t2) Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold compare.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Lt).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: Pos.lt (fstpp t1) (fstpp t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLF.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t1) (fstpp t2)) Lt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.nat_of_P_lt_Lt_compare_complement_morphism.
(* Goal: Peano.lt (Pos.to_nat (fstpp t1)) (Pos.to_nat (fstpp t2)) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Lt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.Pos2Nat.inj_lt.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HCF.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HC.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        apply CompLt.
(* Goal: @Transitive tST ltST *)
        unfold lt.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: Pos.lt (fstpp t1) (fstpp t2) *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt in HLF.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HLF2 : Pos.ltb (fstpp(t2)) (fstpp(t1)) = true).
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_nlt in HLF.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.le_nlt in HLF.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.lt_eq_cases in HLF.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        elim HLF; intro HLF2.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.ltb_lt.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.eqb_neq in HF.
(* Goal: @Logic.eq bool (Pos.ltb (fstpp t2) (fstpp t1)) true *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HLF2 in HF.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HC : compare t1 t2 = Gt).
(* Goal: @Logic.eq comparison (compare t1 t2) Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold compare.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        assert (HCF : Pos.compare (fstpp(t1)) (fstpp(t2)) = Gt).
(* Goal: @Logic.eq comparison (Pos.compare (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        unfold Pos.compare.
(* Goal: Pos.lt (fstpp t2) (fstpp t1) *)
        apply Pos.ltb_lt in HLF2.
(* Goal: @Logic.eq comparison (Pos.compare_cont Eq (fstpp t1) (fstpp t2)) Gt *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.nat_of_P_gt_Gt_compare_complement_morphism.
(* Goal: gt (Pos.to_nat (fstpp t1)) (Pos.to_nat (fstpp t2)) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pnat.Pos2Nat.inj_gt.
(* Goal: Pos.gt (fstpp t1) (fstpp t2) *)
(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        apply Pos.gt_lt_iff.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: @Logic.eq comparison match Pos.compare (fstpp t1) (fstpp t2) with | Eq => Pos.compare (sndpp t1) (sndpp t2) | Lt => Lt | Gt => Gt end Gt *)
(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HCF.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: @CompSpec t eq lt t1 t2 (compare t1 t2) *)
        rewrite HC.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Gt *)
        apply CompGt.
(* Goal: @Transitive tST ltST *)
        unfold lt.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite Pos.eqb_sym in HF.
(* Goal: if Pos.eqb (fstpp t2) (fstpp t1) then Pos.lt (sndpp t2) (sndpp t1) else Pos.lt (fstpp t2) (fstpp t1) *)
        rewrite HF.
(* Goal: Pos.lt (fstpp t2) (fstpp t1) *)
        apply Pos.ltb_lt in HLF2.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.
 Qed.

End SetOfPairsOfPositiveOrderedType.

Module SP := MSetList.Make SetOfPairsOfPositiveOrderedType.
(*
Module SP := MSetAVL.Make SetOfPairsOfPositiveOrderedType.
*)

Module PosOrder <: TotalLeBool.

  Definition t := positive.

  Definition leb := Pos.leb.

  Lemma leb_total : forall p1 p2,
    leb p1 p2 = true \/ leb p2 p1 = true.
  Proof.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
  intros.
(* Goal: or (@eq bool (leb p1 p2) true) (@eq bool (leb p2 p1) true) *)
  do 2 (rewrite Pos.leb_le).
(* Goal: or (Pos.le p1 p2) (Pos.le p2 p1) *)
  do 2 (rewrite Pos.le_lteq).
(* Goal: or (or (Pos.lt p1 p2) (@eq positive p1 p2)) (or (Pos.lt p2 p1) (@eq positive p2 p1)) *)
  assert (HElim := Pos.lt_total p1 p2).
(* Goal: or (or (Pos.lt p1 p2) (@eq positive p1 p2)) (or (Pos.lt p2 p1) (@eq positive p2 p1)) *)
  elim HElim; clear HElim; intro HElim.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
  left; left; assumption.
(* Goal: or (or (Pos.lt p1 p2) (@eq positive p1 p2)) (or (Pos.lt p2 p1) (@eq positive p2 p1)) *)
  elim HElim; clear HElim; intro HElim.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
  left; right; assumption.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
  right; left; assumption.
 Qed.

  Lemma leb_dec : forall p1 p2,
    leb p1 p2 = true \/ leb p1 p2 = false.
  Proof.
(* Goal: forall y : STelt, @eq bool (STmem y STempty) false *)
  intros.
(* Goal: or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
  elim Pos.eq_dec with p1 p2.

(* Goal: forall _ : @eq positive p1 p2, or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
(* Goal: forall _ : not (@eq positive p1 p2), or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
    intro; subst.
(* Goal: or (@eq bool (leb p2 p2) true) (@eq bool (leb p2 p2) false) *)
(* Goal: forall _ : not (@eq positive p1 p2), or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
    left; apply POrderedType.Positive_as_DT.leb_refl.

(* Goal: forall _ : not (@eq positive p1 p2), or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
    intro HNeq.
(* Goal: or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
    elim leb_total with p1 p2; intro Hp1p2.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      left; assumption.

(* Goal: or (@eq bool (leb p1 p2) true) (@eq bool (leb p1 p2) false) *)
        right.
(* Goal: @eq bool (leb p1 p2) false *)
        rewrite Positive_as_DT.leb_gt.
(* Goal: Positive_as_DT.lt p2 p1 *)
        rewrite Positive_as_DT.leb_le in Hp1p2.
(* Goal: Positive_as_DT.lt p2 p1 *)
        rewrite Pos.lt_eq_cases in Hp1p2.
(* Goal: forall (_ : Pos.lt (sndpp x) (sndpp y)) (_ : Pos.lt (fstpp y) (fstpp z)), Pos.lt (fstpp y) (fstpp z) *)
(* Goal: forall (_ : @Logic.eq bool (Pos.eqb (fstpp x) (fstpp y)) false) (_ : Pos.lt (fstpp x) (fstpp y)) (_ : if Pos.eqb (fstpp y) (fstpp z) then Pos.lt (sndpp y) (sndpp z) else Pos.lt (fstpp y) (fstpp z)), if Pos.eqb (fstpp x) (fstpp z) then Pos.lt (sndpp x) (sndpp z) else Pos.lt (fstpp x) (fstpp z) *)
        elim Hp1p2; intro.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          assumption.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          subst; intuition.
 Qed.

End PosOrder.

Module Import PosSort := Sort PosOrder.

Definition OCPAux {n : nat} (cp : cartesianPower positive (S (S n))) := (PosSort.sort (CPToList cp)).

Lemma OCPALengthOK {n : nat} : forall (cp : cartesianPower positive (S (S n))), (length (OCPAux cp)) = (S (S n)).
Proof.
(* Goal: forall cp : tST, eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
intro cp.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (@OCPAux (@n Ar) cp)) (fun n : nat => cartesianPower positive n) (@ListToCP positive (@OCPAux (@n Ar) cp) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCPAux.
(* Goal: @eq nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (S (S n)) *)
assert (HPerm := Permuted_sort (CPToList cp)).
(* Goal: @eq nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (S (S n)) *)
apply Permutation.Permutation_length in HPerm.
(* Goal: @eq nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (S (S n)) *)
rewrite <- HPerm.
(* Goal: @eq nat (@length positive (@CPToList positive (S (S n)) cp)) (S (S n)) *)
apply eq_sym.
(* Goal: @eq nat (S (S n)) (@length positive (@CPToList positive (S (S n)) cp)) *)
apply lengthOfCPToList.
Defined.

Lemma OCPSortedTl :
  forall (l : list positive),
  StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l ->
  StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) (tl l).
Proof.
(* Goal: forall (l : list positive) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) l), @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive l) *)
intros l HSorted.
(* Goal: forall _ : ltList l l, False *)
induction l.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive (@nil positive)) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive (@cons positive a l)) *)
simpl; apply SSorted_nil.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive (@cons positive a l)) *)
clear IHl.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive (@cons positive a l)) *)
simpl; apply StronglySorted_inv in HSorted; destruct HSorted as [HSorted Hhd].
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
assumption.
Qed.

Lemma PermSorted : forall (l l' : list positive),
  Permutation.Permutation l l' ->
  StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l ->
  StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) l' ->
  l = l'.
Proof.
(* Goal: forall _ : ltList l l, False *)
intro l; induction l.

(* Goal: forall (l' : list positive) (_ : @Permutation.Permutation positive (@cons positive a l) l') (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) l'), @eq (list positive) (@cons positive a l) l' *)
  intro l'; induction l'.

(* Goal: @eq bool (STmem y STempty) false *)
    reflexivity.

(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@nil positive)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@nil positive)), @eq (list positive) (@cons positive a l) (@nil positive) *)
(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@cons positive a0 l')) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a0 l')), @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    intro HPerm.
(* Goal: forall (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@nil positive)), @eq (list positive) (@cons positive a l) (@nil positive) *)
(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@cons positive a0 l')) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a0 l')), @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    apply Permutation.Permutation_nil_cons in HPerm.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
    intuition.

(* Goal: forall (l' : list positive) (_ : @Permutation.Permutation positive (@cons positive a l) l') (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) l'), @eq (list positive) (@cons positive a l) l' *)
  intro l'; induction l'.

(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@nil positive)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@nil positive)), @eq (list positive) (@cons positive a l) (@nil positive) *)
(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@cons positive a0 l')) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a0 l')), @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    intro HPerm.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    apply Permutation.Permutation_sym in HPerm.
(* Goal: forall (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@nil positive)), @eq (list positive) (@cons positive a l) (@nil positive) *)
(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@cons positive a0 l')) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a0 l')), @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    apply Permutation.Permutation_nil_cons in HPerm.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
    intuition.

(* Goal: forall (_ : @Permutation.Permutation positive (@cons positive a l) (@cons positive a0 l')) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a l)) (_ : @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@cons positive a0 l')), @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    intros HPerm Hl Hl'.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    assert (HIna' : In a (a :: l)) by (apply in_eq).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    assert (HIna : In a (a0 :: l')) by (apply Permutation.Permutation_in with (a :: l); assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    assert (HIna0' : In a0 (a0 :: l')) by (apply in_eq).
    assert (HIna0 : In a0 (a :: l))
      by (apply Permutation.Permutation_in with (a0 :: l'); apply Permutation.Permutation_sym in HPerm;assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
    clear HIna'; clear HIna0'; apply in_inv in HIna; apply in_inv in HIna0.
    elim HIna; clear HIna; intro HIna; elim HIna0; clear HIna0; intro HIna0;
    try (rewrite HIna in *); try (rewrite <- HIna0 in *).

      assert (HPerm' : Permutation.Permutation l l')
        by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a l') *)
      apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply IHl in HPerm'; try assumption.
(* Goal: @eq bool (STmem y STempty) false *)
      rewrite HPerm'; reflexivity.

      assert (HPerm' : Permutation.Permutation l l')
        by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a l') *)
      apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply IHl in HPerm'; try assumption.
(* Goal: @eq bool (STmem y STempty) false *)
      rewrite HPerm'; reflexivity.

      assert (HPerm' : Permutation.Permutation l l')
        by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a l') *)
      apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply IHl in HPerm'; try assumption.
(* Goal: @eq bool (STmem y STempty) false *)
      rewrite HPerm'; reflexivity.

(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      assert (Hle1 := Hl); assert (Hle2 := Hl').
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      apply StronglySorted_inv in Hle1; apply StronglySorted_inv in Hle2.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      destruct Hle1 as [Hclear Hle1]; clear Hclear; destruct Hle2 as [Hclear Hle2]; clear Hclear.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      assert (Haa0 : (forall x, In x l -> is_true (Pos.leb a x))) by (apply Forall_forall; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      assert (Ha0a : (forall x, In x l' -> is_true (Pos.leb a0 x))) by (apply Forall_forall; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      apply Ha0a in HIna.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      apply Haa0 in HIna0.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      unfold is_true in *.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      apply Pos.leb_le in HIna; apply Pos.leb_le in HIna0.
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a0 l') *)
      assert (H := Pos.le_antisym a0 a HIna HIna0).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      rewrite H in *.
      assert (HPerm' : Permutation.Permutation l l')
        by (apply Permutation.Permutation_app_inv_l with (a :: nil); simpl; assumption).
(* Goal: @eq (list positive) (@cons positive a l) (@cons positive a l') *)
      apply OCPSortedTl in Hl; apply OCPSortedTl in Hl'.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply IHl in HPerm'; try assumption.
(* Goal: @eq bool (STmem y STempty) false *)
      rewrite HPerm'; reflexivity.
Qed.

Definition OCP {n : nat} (cp : cartesianPower positive (S (S n))) : cartesianPower positive (S (S n)).
Proof.
(* Goal: cartesianPower positive (S (S n)) *)
assert (H := OCPALengthOK cp).
(* Goal: cartesianPower positive (S (S n)) *)
rewrite <- H.
(* Goal: cartesianPower positive (@length positive (@OCPAux n cp)) *)
exact (ListToCP (OCPAux cp) (fst cp)).
Defined.

Lemma OCPSortedAux {n : nat} :
  forall (cp : cartesianPower positive (S (S n))),
  StronglySorted (fun x x0 : positive => is_true (x <=? x0)%positive) (CPToList (OCP cp)).
Proof.
(* Goal: forall cp : cartesianPower positive (S (S n)), @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n cp)) *)
intros cp.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCP.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (@OCPAux (@n Ar) cp)) (fun n : nat => cartesianPower positive n) (@ListToCP positive (@OCPAux (@n Ar) cp) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCPAux.
(* Goal: iff (@In positive p (@CPToList positive (S (S n)) cp)) (@In positive p (@CPToList positive (S (S n)) (@eq_rect nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (fun n : nat => cartesianPower positive n) (@ListToCP positive (sort (@CPToList positive (S (S n)) cp)) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp)) (S (S n)) (@OCPALengthOK n cp)))) *)
elim_eq_rect; simpl.
(* Goal: eqList (@CPToList positive (@length positive (@OCPAux (@n Ar) cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
rewrite CPLOK.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) n (@tailCP positive n cp)))) *)
apply StronglySorted_sort.
(* Goal: @Transitive positive (fun x x0 : positive => is_true (Pos.leb x x0)) *)
intros x1 x2 x3.
(* Goal: forall (_ : is_true (Pos.leb x1 x2)) (_ : is_true (Pos.leb x2 x3)), is_true (Pos.leb x1 x3) *)
unfold is_true.
(* Goal: forall (_ : @eq bool (Pos.leb x1 x2) true) (_ : @eq bool (Pos.leb x2 x3) true), @eq bool (Pos.leb x1 x3) true *)
intros Hx1x2 Hx2x3.
(* Goal: @eq bool (Pos.leb x1 x3) true *)
apply Pos.leb_le in Hx1x2.
(* Goal: @eq bool (Pos.leb x1 x3) true *)
apply Pos.leb_le in Hx2x3.
(* Goal: @eq bool (Pos.leb x1 x3) true *)
apply Pos.leb_le.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
transitivity x2; assumption.
Qed.

Lemma OCPPerm {n : nat} :
  forall (cp : cartesianPower positive (S (S n))),
  Permutation.Permutation (CPToList cp) (CPToList (OCP cp)).
Proof.
(* Goal: forall cp : tST, eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
intro cp.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCP.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (@OCPAux (@n Ar) cp)) (fun n : nat => cartesianPower positive n) (@ListToCP positive (@OCPAux (@n Ar) cp) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCPAux.
(* Goal: iff (@In positive p (@CPToList positive (S (S n)) cp)) (@In positive p (@CPToList positive (S (S n)) (@eq_rect nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (fun n : nat => cartesianPower positive n) (@ListToCP positive (sort (@CPToList positive (S (S n)) cp)) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp)) (S (S n)) (@OCPALengthOK n cp)))) *)
elim_eq_rect; simpl.
(* Goal: eqList (@CPToList positive (@length positive (@OCPAux (@n Ar) cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
rewrite CPLOK.
(* Goal: @Permutation.Permutation positive (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) n (@tailCP positive n cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) n (@tailCP positive n cp)))) *)
apply Permuted_sort.
Qed.

Lemma CPLOCPTlOK {n : nat} :
  forall (cp : cartesianPower positive (S (S (S n)))),
  headCP cp = headCP (OCP cp) ->
  CPToList (OCP (tailCP cp)) = CPToList (tailCP (OCP cp)).
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (S n)))) (_ : @eq positive (@headCP positive (S (S n)) cp) (@headCP positive (S (S n)) (@OCP (S n) cp))), @eq (cartesianPower positive (S (S n))) (@OCP n (@tailCP positive (S n) cp)) (@tailCP positive (S n) (@OCP (S n) cp)) *)
intros cp Hhd.
(* Goal: @eq (list positive) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
apply PermSorted.

(* Goal: @Permutation.Permutation positive (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  assert (H := OCPPerm cp).
(* Goal: @Permutation.Permutation positive (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  rewrite CPToListOK in H.
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.Permutation_sym in H.
(* Goal: @Permutation.Permutation positive (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  rewrite CPToListOK in H.
(* Goal: @Permutation.Permutation positive (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  rewrite <- Hhd in H.
(* Goal: @Permutation.Permutation positive (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.Permutation_app_inv_l with ((headCP cp) :: nil).
  assert (H' : (headCP cp :: nil) ++ CPToList (OCP (tailCP cp)) = headCP cp :: (CPToList (OCP (tailCP cp))))
    by (simpl; reflexivity); rewrite H'; clear H'.
  assert (H' : (headCP cp :: nil) ++ CPToList (tailCP (OCP cp)) = headCP cp :: (CPToList (tailCP (OCP cp))))
    by (simpl; reflexivity); rewrite H'; clear H'.
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.Permutation_sym in H.
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp)))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.perm_trans with (headCP cp :: CPToList (tailCP cp)); try assumption; clear H.
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  assert (H := OCPPerm (tailCP cp)).
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.Permutation_sym in H.
(* Goal: @Permutation.Permutation positive (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp)))) (@cons positive (@headCP positive (S (S n)) cp) (@CPToList positive (S (S n)) (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@OCP n (@tailCP positive (S n) cp))) *)
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  apply Permutation.perm_skip.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
  assumption.

(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S (S n))) (@OCP (S n) cp)) *)
  apply OCPSortedAux.

(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S n)) (@tailCP positive (S n) (@OCP (S n) cp))) *)
  rewrite <- CPToListTl2.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@tl positive (@CPToList positive (S (S (S n))) (@OCP (S n) cp))) *)
  apply OCPSortedTl.
(* Goal: @StronglySorted positive (fun x x0 : positive => is_true (Pos.leb x x0)) (@CPToList positive (S (S (S n))) (@OCP (S n) cp)) *)
  apply OCPSortedAux.
Qed.

Lemma OCPTlOK {n : nat} :
  forall (cp : cartesianPower positive (S (S (S n)))),
  headCP cp = headCP (OCP cp) ->
  OCP (tailCP cp) = tailCP (OCP cp).
Proof.
(* Goal: forall (cp : cartesianPower positive (S (S (S n)))) (_ : @eq positive (@headCP positive (S (S n)) cp) (@headCP positive (S (S n)) (@OCP (S n) cp))), @eq (cartesianPower positive (S (S n))) (@OCP n (@tailCP positive (S n) cp)) (@tailCP positive (S n) (@OCP (S n) cp)) *)
intros cp Hhd.
(* Goal: @eq (cartesianPower positive (S (S n))) (@OCP n (@tailCP positive (S n) cp)) (@tailCP positive (S n) (@OCP (S n) cp)) *)
apply CPLOCPTlOK in Hhd.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
apply CPLCP; assumption.
Qed.

Lemma InCPOCP {n : nat} : forall p (cp : cartesianPower positive (S (S n))),
  InCP p cp <-> InCP p (OCP cp).
Proof.
(* Goal: forall (p : positive) (cp : cartesianPower positive (S (S n))), iff (@InCP positive (S (S n)) p cp) (@InCP positive (S (S n)) p (@OCP n cp)) *)
intros p cp.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCP.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (@OCPAux (@n Ar) cp)) (fun n : nat => cartesianPower positive n) (@ListToCP positive (@OCPAux (@n Ar) cp) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
unfold OCPAux.
(* Goal: iff (@InCP positive (S (S n)) p cp) (@InCP positive (S (S n)) p (@eq_rect nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (fun n : nat => cartesianPower positive n) (@ListToCP positive (sort (@CPToList positive (S (S n)) cp)) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp)) (S (S n)) (@OCPALengthOK n cp))) *)
unfold InCP.
(* Goal: iff (@In positive p (@CPToList positive (S (S n)) cp)) (@In positive p (@CPToList positive (S (S n)) (@eq_rect nat (@length positive (sort (@CPToList positive (S (S n)) cp))) (fun n : nat => cartesianPower positive n) (@ListToCP positive (sort (@CPToList positive (S (S n)) cp)) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp)) (S (S n)) (@OCPALengthOK n cp)))) *)
elim_eq_rect; simpl.
(* Goal: iff (or (@eq positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) n (@tailCP positive n cp)))) (@In positive p (@CPToList positive (@length positive (@OCPAux n cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) n (@tailCP positive n cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp)))) *)
induction n.

(* Goal: eqList (@CPToList positive (@length positive (@OCPAux (@n Ar) cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
  rewrite CPLOK.
(* Goal: iff (or (@eq positive (@fst positive positive cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) O (@tailCP positive O cp)))) (@In positive p (sort (@cons positive (@fst positive positive cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) O (@tailCP positive O cp))))) *)
(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (@CPToList positive (@length positive (@OCPAux (S n) cp)) (@ListToCP positive (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)))) *)
  assert (HPerm1 := Permuted_sort (CPToList cp)); simpl in HPerm1.
(* Goal: iff (or (@eq positive (@fst positive positive cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) O (@tailCP positive O cp)))) (@In positive p (sort (@cons positive (@fst positive positive cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) O (@tailCP positive O cp))))) *)
(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (@CPToList positive (@length positive (@OCPAux (S n) cp)) (@ListToCP positive (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)))) *)
  assert (HPerm2 := HPerm1); apply Permutation.Permutation_sym in HPerm2.
  assert (HInOK : In p (sort (fst cp :: snd cp :: nil)) <-> In p (fst cp :: snd cp :: nil))
    by (split; intro HIn; try (apply Permutation.Permutation_in with (sort (fst cp :: snd cp :: nil)); assumption);
                          apply Permutation.Permutation_in with (fst cp :: snd cp :: nil); assumption).
(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))))) *)
  split; intro HIn.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    apply HInOK; simpl; assumption.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    apply HInOK in HIn; simpl in HIn; assumption.

(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (@CPToList positive (@length positive (@OCPAux (S n) cp)) (@ListToCP positive (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)))) *)
  clear IHn.
(* Goal: eqList (@CPToList positive (@length positive (@OCPAux (@n Ar) cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
  rewrite CPLOK.
  set (sscp := (nat_rect (fun n : nat => cartesianPower positive (S n) -> list positive)
                       (fun cp0 : cartesianPower positive 1 => cp0 :: nil)
                       (fun (n : nat) (IHn : cartesianPower positive (S n) -> list positive)
                       (cp0 : cartesianPower positive (S (S n))) =>
                       fst cp0 :: IHn (tailCP cp0)) n (tailCP (snd cp)))).
(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))))) *)
  assert (HPerm := Permuted_sort (fst cp :: fst (snd cp) :: sscp)).
(* Goal: iff (or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) (@In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))))) *)
  split; intro HIn.

(* Goal: @In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    elim HIn; clear HIn; intro HIn.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
      subst.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption.
(* Goal: @In positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@tailCP positive (S n) cp)) (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)) sscp) *)
(* Goal: @In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      apply in_eq.

(* Goal: @In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      elim HIn; clear HIn; intro HIn.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption.
(* Goal: @In positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@tailCP positive (S n) cp)) (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)) sscp)) *)
(* Goal: @In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply in_cons.
(* Goal: @In positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@tailCP positive (S n) cp)) (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)) sscp) *)
(* Goal: @In positive p (sort (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp)))) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply in_eq.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply Permutation.Permutation_in with (fst cp :: fst (snd cp) :: sscp); try assumption.
(* Goal: @In positive p (@cons positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) (@snd positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp)) sscp)) *)
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        do 2 (apply in_cons).
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        assumption.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    apply Permutation.Permutation_sym in HPerm.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    assert (HInOKAux := Permutation.Permutation_in).
    assert (HInOK := HInOKAux positive (sort (fst cp :: fst (snd cp) :: sscp))
                                       (fst cp :: fst (snd cp) :: sscp) p HPerm HIn); clear HInOKAux; clear HIn.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    rename HInOK into HIn.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    assumption.
Qed.


Section Set_of_tuple_of_positive.

  Context {Ar : Arity}.

  Fixpoint eqList (l1 l2 : list positive) :=
    match l1, l2 with
      | nil, nil => True
      | (hd1 :: tl1), (hd2 :: tl2) => (Pos.eq hd1 hd2) /\ (eqList tl1 tl2)
      | _, _ => False
    end.

  Lemma eqListRefl : forall l, eqList l l.
  Proof.
(* Goal: forall l : list positive, eqList l l *)
    intro l; induction l; simpl.

(* Goal: True *)
      trivial.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
      split; try assumption.
(* Goal: @eq bool (STmem y STempty) false *)
      reflexivity.
  Qed.

  Lemma eqListSym : forall l l', eqList l l' -> eqList l' l.
  Proof.
(* Goal: forall _ : ltList l l, False *)
    intro l; induction l.

(* Goal: forall (l' : list positive) (_ : eqList (@cons positive a l) l'), eqList l' (@cons positive a l) *)
      intro l'; induction l'; auto.

(* Goal: forall (l' : list positive) (_ : eqList (@cons positive a l) l'), eqList l' (@cons positive a l) *)
      intro l'; induction l'; auto.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
      simpl.
(* Goal: forall _ : and (Pos.eq a a0) (eqList l l'), and (Pos.eq a0 a) (eqList l' l) *)
      intro H.
(* Goal: and (Pos.eq a0 a) (eqList l' l) *)
      destruct H as [Haa0 Hll'].
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      split; intuition.
  Qed.

  Lemma eqListTrans : forall l1 l2 l3, eqList l1 l2 -> eqList l2 l3 -> eqList l1 l3.
  Proof.
(* Goal: forall (l1 l2 l3 : list positive) (_ : eqList l1 l2) (_ : eqList l2 l3), eqList l1 l3 *)
    intro l1; induction l1.

(* Goal: forall (l2 l3 : list positive) (_ : eqList (@cons positive a l1) l2) (_ : eqList l2 l3), eqList (@cons positive a l1) l3 *)
      intro l2; induction l2.

(* Goal: forall (l3 : list positive) (_ : eqList (@cons positive a l1) (@cons positive a0 l2)) (_ : eqList (@cons positive a0 l2) l3), eqList (@cons positive a l1) l3 *)
        intro l3; induction l3.

(* Goal: True *)
          simpl; trivial.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          simpl; intuition.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        simpl; intuition.

(* Goal: forall (l2 l3 : list positive) (_ : eqList (@cons positive a l1) l2) (_ : eqList l2 l3), eqList (@cons positive a l1) l3 *)
      intro l2; induction l2.

(* Goal: forall (l3 : list positive) (_ : eqList (@cons positive a l1) (@cons positive a0 l2)) (_ : eqList (@cons positive a0 l2) l3), eqList (@cons positive a l1) l3 *)
        intro l3; induction l3.

(* Goal: True *)
          simpl; trivial.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          simpl; intuition.

(* Goal: forall (l3 : list positive) (_ : eqList (@cons positive a l1) (@cons positive a0 l2)) (_ : eqList (@cons positive a0 l2) l3), eqList (@cons positive a l1) l3 *)
        intro l3; induction l3.

(* Goal: True *)
          simpl; trivial.

(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: forall (_ : and (Pos.eq a a0) (eqList l1 l2)) (_ : and (Pos.eq a0 a1) (eqList l2 l3)), and (Pos.eq a a1) (eqList l1 l3) *)
          intros Hl1l2 Hl2l3.
(* Goal: and (Pos.eq a a1) (eqList l1 l3) *)
          destruct Hl1l2 as [Haa0 Hl1l2].
(* Goal: and (Pos.eq a a1) (eqList l1 l3) *)
          destruct Hl2l3 as [Ha0a1 Hl2l3].
(* Goal: and (Pos.eq a a1) (eqList l1 l3) *)
          split.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
            transitivity a0; assumption.

(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
            apply IHl1 with l2; assumption.
  Qed.

  Definition tST := cartesianPower positive (S (S n)).

  Definition eqST (cp1 cp2 : tST) :=
    eqList (PosSort.sort (CPToList cp1)) (PosSort.sort (CPToList cp2)).

  Lemma eqListSortOCP : forall (cp : tST), eqList (CPToList (OCP cp)) (PosSort.sort (CPToList cp)).
  Proof.
(* Goal: forall cp : tST, eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
    intro cp.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@OCP (@n Ar) cp)) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
    unfold OCP.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (@OCPAux (@n Ar) cp)) (fun n : nat => cartesianPower positive n) (@ListToCP positive (@OCPAux (@n Ar) cp) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
    unfold OCPAux.
(* Goal: eqList (@CPToList positive (S (S (@n Ar))) (@eq_rect nat (@length positive (sort (@CPToList positive (S (S (@n Ar))) cp))) (fun n : nat => cartesianPower positive n) (@ListToCP positive (sort (@CPToList positive (S (S (@n Ar))) cp)) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp)) (S (S (@n Ar))) (@OCPALengthOK (@n Ar) cp))) (sort (@CPToList positive (S (S (@n Ar))) cp)) *)
    elim_eq_rect.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
    simpl.
(* Goal: eqList (@CPToList positive (@length positive (@OCPAux (@n Ar) cp)) (@ListToCP positive (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
    rewrite CPLOK.
(* Goal: eqList (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) (sort (@cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive (@n Ar)) cp) (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (@n Ar) (@tailCP positive (@n Ar) cp)))) *)
    apply eqListRefl.
  Qed.

  Fixpoint eqbList (l1 l2 : list positive) :=
    match l1, l2 with
      | nil         , nil          => true
      | (hd1 :: tl1), (hd2 :: tl2) => (Pos.eqb hd1 hd2) && (eqbList tl1 tl2)
      | _           , _            => false
    end.

  Lemma eqbListEqList : forall l1 l2, eqbList l1 l2 = true <-> eqList l1 l2.
  Proof.
(* Goal: forall l1 l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    intro l1.
(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    induction l1.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@nil positive)) true) (eqList (@cons positive a l1) (@nil positive)) *)
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        simpl; unfold eqList.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@nil positive)) true) (eqList (@cons positive a l1) (@nil positive)) *)
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        simpl; unfold eqList.
(* Goal: iff (@eq bool false true) False *)
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        split; intro; intuition; discriminate.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@nil positive)) true) (eqList (@cons positive a l1) (@nil positive)) *)
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        simpl; unfold eqList.
(* Goal: iff (@eq bool false true) False *)
(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        split; intro; intuition; discriminate.

(* Goal: iff (@eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true) (eqList (@cons positive a l1) (@cons positive a0 l2)) *)
        split; intro H.

(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          unfold eqbList in H.
(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          apply andb_true_iff in H.
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          destruct H as [Hhd Htl].
(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          fold eqbList in Htl.
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          assert (H := IHl1 l2).
(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          rewrite H in Htl.
(* Goal: eqList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          unfold eqList.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          split; try assumption.
(* Goal: Pos.eq a a0 *)
(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          rewrite PositiveSet.E.eqb_eq in Hhd.
(* Goal: @eq bool (STmem y STempty) false *)
          subst; reflexivity.

(* Goal: @eq bool (eqbList (@cons positive a l1) (@cons positive a0 l2)) true *)
          apply andb_true_iff.
(* Goal: and (@eq bool (Pos.eqb a a0) true) (@eq bool ((fix eqbList (l1 l2 : list positive) {struct l1} : bool := match l1 with | nil => match l2 with | nil => true | cons p l => false end | cons hd1 tl1 => match l2 with | nil => false | cons hd2 tl2 => andb (Pos.eqb hd1 hd2) (eqbList tl1 tl2) end end) l1 l2) true) *)
          rewrite PositiveSet.E.eqb_eq; fold eqbList.
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          unfold eqList in H.
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          destruct H as [Hhd Htl].
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          fold eqList in Htl.
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          assert (H := IHl1 l2).
(* Goal: and (@eq positive a a0) (@eq bool (eqbList l1 l2) true) *)
          rewrite <- H in Htl.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          split; assumption.
  Qed.

  Definition eqbST (cp1 cp2 : tST) :=
    eqbList (PosSort.sort (CPToList cp1)) (PosSort.sort (CPToList cp2)).

  Lemma eqbST_eqST : forall cp1 cp2, eqbST cp1 cp2 = true <-> eqST cp1 cp2.
  Proof. intros; unfold eqbST, eqST; apply eqbListEqList. Qed.

  Fixpoint ltList (l1 l2 : list positive) :=
    match l1, l2 with
      | nil, nil => False
      | (hd1 :: tl1), (hd2 :: tl2) => if (Pos.ltb hd1 hd2) then True
                                      else if (Pos.ltb hd2 hd1) then False
                                           else (ltList tl1 tl2)
      | nil, _ => True
      | _, nil => False
    end.

  Lemma lengthOne : forall (l : list positive),
    length l = 1 -> exists a, l = a :: nil.
  Proof.
(* Goal: forall (l : list positive) (_ : @eq nat (@length positive l) (S O)), @ex positive (fun a : positive => @eq (list positive) l (@cons positive a (@nil positive))) *)
    intros l Hl.
(* Goal: forall _ : ltList l l, False *)
    induction l.

(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@nil positive) (@cons positive a0 l0))) *)
(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@cons positive a l) (@cons positive a0 l0))) *)
      simpl in Hl; discriminate.

(* Goal: forall _ : ltList l l, False *)
      induction l.

(* Goal: @eq bool (STmem y STempty) false *)
        exists a; reflexivity.

(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@nil positive) (@cons positive a0 l0))) *)
(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@cons positive a l) (@cons positive a0 l0))) *)
      simpl in Hl; discriminate.
  Qed.

  Lemma lengthAtLeastOne : forall (l : list positive) n,
    length l = (S n) -> exists a0 l0, l = a0 :: l0.
  Proof.
(* Goal: forall (l : list positive) (n : nat) (_ : @eq nat (@length positive l) (S n)), @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) l (@cons positive a0 l0))) *)
    intros l n Hl.
(* Goal: forall _ : ltList l l, False *)
    induction l.

(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@nil positive) (@cons positive a0 l0))) *)
(* Goal: @ex positive (fun a0 : positive => @ex (list positive) (fun l0 : list positive => @eq (list positive) (@cons positive a l) (@cons positive a0 l0))) *)
      simpl in Hl; discriminate.

(* Goal: @eq bool (STmem y STempty) false *)
      exists a; exists l; reflexivity.
  Qed.

  Lemma ltListTrans : forall m x y z,
    length x = (S m) ->
    length y = (S m) ->
    length z = (S m) ->
    ltList x y -> ltList y z -> ltList x z.
  Proof.
(* Goal: forall (m : nat) (x y z : list positive) (_ : @eq nat (@length positive x) (S m)) (_ : @eq nat (@length positive y) (S m)) (_ : @eq nat (@length positive z) (S m)) (_ : ltList x y) (_ : ltList y z), ltList x z *)
    intro m; induction m; intros x y z lx ly lz Hxy Hyz.

(* Goal: ltList x z *)
(* Goal: ltList x z *)
      assert (Hx := lengthOne x lx); destruct Hx as [hdx Hx].
(* Goal: ltList x z *)
(* Goal: ltList x z *)
      assert (Hy := lengthOne y ly); destruct Hy as [hdy Hy].
(* Goal: ltList x z *)
(* Goal: ltList x z *)
      assert (Hz := lengthOne z lz); destruct Hz as [hdz Hz].
(* Goal: ltList x z *)
      subst; simpl in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else False *)
(* Goal: ltList x z *)
      assert (H : Pos.ltb hdx hdz = true).

(* Goal: @eq bool (Pos.ltb hdx hdz) true *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else False *)
(* Goal: ltList x z *)
        rewrite Pos.ltb_lt.
(* Goal: Pos.lt hdx hdz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else False *)
(* Goal: ltList x z *)
        transitivity hdy.

(* Goal: Pos.lt hdy hdz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else False *)
(* Goal: ltList x z *)
          rewrite <- Pos.ltb_lt.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          induction (Pos.ltb hdx hdy); intuition.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          induction (Pos.ltb hdy hdx); intuition.

(* Goal: Pos.lt hdy hdz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else False *)
(* Goal: ltList x z *)
          rewrite <- Pos.ltb_lt.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          induction (Pos.ltb hdy hdz); intuition.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          induction (Pos.ltb hdz hdy); intuition.

(* Goal: True *)
        rewrite H; trivial.

(* Goal: ltList x z *)
      assert (Hx := lengthAtLeastOne x (S m) lx); destruct Hx as [hdx [tlx Hx]].
(* Goal: ltList x z *)
      assert (Hy := lengthAtLeastOne y (S m) ly); destruct Hy as [hdy [tly Hy]].
(* Goal: ltList x z *)
      assert (Hz := lengthAtLeastOne z (S m) lz); destruct Hz as [hdz [tlz Hz]].
(* Goal: ltList x z *)
      subst; simpl in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HEqxy := Pos.compare_eq hdx hdy).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HEqyz := Pos.compare_eq hdy hdz).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HLtxy := Pos.compare_nge_iff hdx hdy).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HLtyz := Pos.compare_nge_iff hdy hdz).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HGtxy := Pos.compare_gt_iff hdx hdy).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      assert (HGtyz := Pos.compare_gt_iff hdy hdz).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      induction (Pos.compare hdx hdy); induction (Pos.compare hdy hdz).

(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Eq = Eq) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H' : Eq = Eq) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HEqyz in H'; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: if Pos.ltb hdz hdz then True else if Pos.ltb hdz hdz then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H := Pos.ltb_irrefl hdz).
(* Goal: if Pos.ltb hdz hdz then True else if Pos.ltb hdz hdz then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *; clear H.
(* Goal: ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply eq_add_S in lx.
(* Goal: ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply eq_add_S in ly.
(* Goal: ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply eq_add_S in lz.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
        apply IHm with tly; assumption.

(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Eq = Eq) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H' : Lt = Lt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HLtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite <- Pos.lt_nle in H'.
(* Goal: if Pos.ltb hdy hdz then True else if Pos.ltb hdz hdy then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite <- Pos.ltb_lt in H'.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: True *)
        trivial.

(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Eq = Eq) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HEqxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H' : Gt = Gt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HGtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: if Pos.ltb hdy hdz then True else if Pos.ltb hdz hdy then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite <- Pos.ltb_lt in H'.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: True *)
        trivial.

(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Lt = Lt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HLtxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H' : Eq = Eq) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HEqyz in H'; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        rewrite <- Pos.lt_nle in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        rewrite <- Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *.
(* Goal: True *)
        trivial.

(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Lt = Lt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HLtxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H' : Lt = Lt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HLtyz in H'; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        rewrite <- Pos.lt_nle in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite <- Pos.lt_nle in H'.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H'' : Pos.lt hdx hdz) by (transitivity hdy; assumption).
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite <- Pos.ltb_lt in H''.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H''.
(* Goal: True *)
        trivial.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Gt = Gt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HGtyz in H; clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        rewrite <- Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.lt_nle in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H' : Pos.ltb hdy hdz = false).

(* Goal: @eq bool (Pos.ltb hdx hdy) false *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          rewrite Pos.ltb_nlt.
(* Goal: not (Pos.lt hdx hdy) *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          intro H'.
(* Goal: False *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply H.
(* Goal: Pos.le hdx hdy *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply Pos.lt_eq_cases.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          left; assumption.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Gt = Gt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        rewrite <- Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.lt_nle in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H' : Pos.ltb hdx hdy = false).

(* Goal: @eq bool (Pos.ltb hdx hdy) false *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          rewrite Pos.ltb_nlt.
(* Goal: not (Pos.lt hdx hdy) *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          intro H'.
(* Goal: False *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply H.
(* Goal: Pos.le hdx hdy *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply Pos.lt_eq_cases.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          left; assumption.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Gt = Gt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        rewrite <- Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.lt_nle in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H' : Pos.ltb hdx hdy = false).

(* Goal: @eq bool (Pos.ltb hdx hdy) false *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          rewrite Pos.ltb_nlt.
(* Goal: not (Pos.lt hdx hdy) *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          intro H'.
(* Goal: False *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply H.
(* Goal: Pos.le hdx hdy *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply Pos.lt_eq_cases.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          left; assumption.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        clear HEqyz; clear HLtyz; clear HGtyz.
(* Goal: @eq bool (STmem y STempty) false *)
        assert (H : Gt = Gt) by reflexivity.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        apply HGtxy in H; clear HEqxy; clear HLtxy; clear HGtxy.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        rewrite <- Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.ltb_lt in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite Pos.lt_nle in H.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        assert (H' : Pos.ltb hdx hdy = false).

(* Goal: @eq bool (Pos.ltb hdx hdy) false *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          rewrite Pos.ltb_nlt.
(* Goal: not (Pos.lt hdx hdy) *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          intro H'.
(* Goal: False *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply H.
(* Goal: Pos.le hdx hdy *)
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
          apply Pos.lt_eq_cases.
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
          left; assumption.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        rewrite H' in *.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        intuition.
  Qed.

  Lemma sortOK : forall m l, length l = m -> length (sort l) = m.
  Proof.
(* Goal: forall (m : nat) (l : list positive) (_ : @eq nat (@length positive l) m), @eq nat (@length positive (sort l)) m *)
    intros m l Hl.
(* Goal: @eq nat (@length positive (sort l)) m *)
    assert (H := Permuted_iter_merge l nil).
(* Goal: @eq nat (@length positive (sort l)) m *)
    apply Permutation.Permutation_length in H.
(* Goal: @eq nat (@length positive (sort l)) m *)
    unfold flatten_stack in H.
(* Goal: @eq nat (@length positive (sort l)) m *)
    simpl in H.
(* Goal: @eq nat (@length positive (sort l)) m *)
    rewrite <- Hl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
    rewrite H.
(* Goal: @eq nat (@length positive (sort l)) (@length positive (iter_merge (@nil (option (list positive))) l)) *)
    unfold sort.
(* Goal: @eq bool (STmem y STempty) false *)
    reflexivity.
  Qed.

  Definition ltST (cp1 cp2 : tST) :=
    ltList (PosSort.sort (CPToList cp1)) (PosSort.sort (CPToList cp2)).

  Lemma ltTrans : Transitive ltST.
  Proof.
(* Goal: @Transitive tST ltST *)
    unfold lt.
(* Goal: @Transitive tST ltST *)
    intros x y z Hxy Hyz.

(* Goal: @eq bool (STmem y STempty) false *)
    assert (lx : (S (S n)) = (S (S n))) by reflexivity.
(* Goal: ltST x z *)
    assert (lx' := lengthOfCPToList x).
(* Goal: ltST x z *)
    assert (lx'' := sortOK (S (S n)) (CPToList x)).
(* Goal: ltST x z *)
    rewrite <- lx' in lx''; clear lx'.
(* Goal: ltST x z *)
    apply lx'' in lx; clear lx''.

(* Goal: @eq bool (STmem y STempty) false *)
    assert (ly : (S (S n)) = (S (S n))) by reflexivity.
(* Goal: ltST x z *)
    assert (ly' := lengthOfCPToList y).
(* Goal: ltST x z *)
    assert (ly'' := sortOK (S (S n)) (CPToList y)).
(* Goal: ltST x z *)
    rewrite <- ly' in ly''; clear ly'.
(* Goal: ltST x z *)
    apply ly'' in ly; clear ly''.

(* Goal: @eq bool (STmem y STempty) false *)
    assert (lz : (S (S n)) = (S (S n))) by reflexivity.
(* Goal: ltST x z *)
    assert (lz' := lengthOfCPToList z).
(* Goal: ltST x z *)
    assert (lz'' := sortOK (S (S n)) (CPToList z)).
(* Goal: ltST x z *)
    rewrite <- lz' in lz''; clear lz'.
(* Goal: ltST x z *)
    apply lz'' in lz; clear lz''.

(* Goal: ltST x z *)
    assert (H := ltListTrans (S n) (sort (CPToList x)) (sort (CPToList y)) (sort (CPToList z))).
(* Goal: or (@eq positive (@fst positive (prod positive ((fix cartesianPowerAux (T : Type) (n : nat) {struct n} : Type := match n with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n)) cp) p) (@In positive p (nat_rect (fun n : nat => forall _ : cartesianPower positive (S n), list positive) (fun cp : cartesianPower positive (S O) => @cons (cartesianPower positive (S O)) cp (@nil (cartesianPower positive (S O)))) (fun (n : nat) (IHn : forall _ : cartesianPower positive (S n), list positive) (cp : cartesianPower positive (S (S n))) => @cons positive (@fst positive ((fix cartesianPowerAux (T : Type) (n0 : nat) {struct n0} : Type := match n0 with | O => T | S p => prod T (cartesianPowerAux T p) end) positive n) cp) (IHn (@tailCP positive n cp))) (S n) (@tailCP positive (S n) cp))) *)
    apply H; assumption.
  Qed.

  Lemma ltListIrrefl : forall l, ltList l l -> False.
  Proof.
(* Goal: forall (l : list positive) (_ : ltList l l), False *)
    intro l.
(* Goal: forall _ : ltList l l, False *)
    induction l.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      simpl; intuition.

(* Goal: forall _ : ltList (@cons positive a l) (@cons positive a l), False *)
      assert (H := Pos.lt_irrefl a).
(* Goal: forall _ : ltList (@cons positive a l) (@cons positive a l), False *)
      rewrite <- Pos.ltb_nlt in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
      simpl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
      rewrite H.
(* Goal: forall _ : ltList l l, False *)
      apply IHl.
  Qed.

  Lemma eqListOK : forall l1 l2, eqList l1 l2 -> l1 = l2.
  Proof.
(* Goal: forall l1 l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    intro l1.
(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    induction l1.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: True *)
        trivial.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        simpl; intuition.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
        simpl; intuition.

(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        simpl.
(* Goal: forall _ : and (Pos.eq a a0) (eqList l1 l2), @eq (list positive) (@cons positive a l1) (@cons positive a0 l2) *)
        intro HEq.
(* Goal: @eq (list positive) (@cons positive a l1) (@cons positive a0 l2) *)
        destruct HEq as [Hhd Htl].
(* Goal: @eq (list positive) (@cons positive a l1) (@cons positive a0 l2) *)
        unfold Pos.eq in Hhd.
(* Goal: @eq (list positive) (@cons positive a l1) (@cons positive a0 l2) *)
        apply IHl1 in Htl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        subst.
(* Goal: @eq bool (STmem y STempty) false *)
        reflexivity.
  Qed.

  Fixpoint compareList (l1 l2 : list positive) :=
    match l1, l2 with
    | nil, nil => Eq
    | (hd1 :: tl1), (hd2 :: tl2) => match Pos.compare hd1 hd2 with
                                    | Lt => Lt
                                    | Eq => compareList tl1 tl2
                                    | Gt => Gt
                                    end
    | nil, _ => Lt
    | _, nil => Gt
    end.

  Lemma compareListSpec : forall l1 l2,
    CompSpec eqList ltList l1 l2 (compareList l1 l2).
  Proof.
(* Goal: forall l1 l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    intro l1.
(* Goal: @Transitive tST ltST *)
    unfold eqST; unfold lt.
(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList l1 l2 (compareList l1 l2) *)
    induction l1.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        simpl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Eq *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Gt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        apply CompEq.
(* Goal: True *)
        simpl; trivial.

(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        simpl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        apply CompLt.
(* Goal: True *)
        simpl; trivial.

(* Goal: forall l2 : list positive, @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      intro l2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) l2 (compareList (@cons positive a l1) l2) *)
      induction l2.

(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
        simpl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Gt *)
        apply CompGt.
(* Goal: True *)
        simpl; trivial.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        clear IHl2.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        assert (HEq := Pos.compare_eq a a0).
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        assert (HLt := Pos.compare_nge_iff a a0).
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        assert (HGt := Pos.compare_gt_iff a a0).
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
        induction (Pos.compare a a0).

(* Goal: @eq bool (STmem y STempty) false *)
          assert (H : Eq = Eq) by reflexivity.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply HEq in H; clear HEq; clear HLt; clear HGt.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          subst.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) match Pos.compare a0 a0 with | Eq => compareList l1 l2 | Lt => Lt | Gt => Gt end *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          rewrite POrderedType.Positive_as_OT.compare_refl.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) (compareList l1 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          assert (H := IHl1 l2); clear IHl1.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) (compareList l1 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          induction H.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Eq *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Gt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
            apply CompEq.
(* Goal: eqList (@cons positive a0 l1) (@cons positive a0 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a0 l1) (@cons positive a0 l2) Gt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
            simpl; split; auto; apply Pos.eq_refl.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
            apply CompLt.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a0 l1) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
            simpl; rewrite Pos.ltb_irrefl; auto.

(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Gt *)
            apply CompGt.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a0 l1) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
            simpl; rewrite Pos.ltb_irrefl; auto.

(* Goal: @eq bool (STmem y STempty) false *)
          assert (H : Lt = Lt) by reflexivity.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply HLt in H; clear HEq; clear HLt; clear HGt.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          rewrite <- Pos.lt_nle in H.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply Pos.compare_lt_iff in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
          rewrite H.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Lt *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply CompLt.
(* Goal: ltList (@cons positive a l1) (@cons positive a0 l2) *)
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          rewrite Pos.compare_lt_iff in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          rewrite <- Pos.ltb_lt in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
          rewrite H.
(* Goal: True *)
          trivial.

(* Goal: @eq bool (STmem y STempty) false *)
          assert (H : Gt = Gt) by reflexivity.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply HGt in H; clear HEq; clear HLt; clear HGt.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) (compareList (@cons positive a l1) (@cons positive a0 l2)) *)
          apply Pos.compare_gt_iff in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
          rewrite H.
(* Goal: @CompSpec (list positive) eqList ltList (@cons positive a l1) (@cons positive a0 l2) Gt *)
          apply CompGt.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          rewrite Pos.compare_gt_iff in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          rewrite <- Pos.ltb_lt in H.
(* Goal: ltList (@cons positive a0 l2) (@cons positive a l1) *)
          simpl.
(* Goal: if Pos.ltb a0 a then True else if Pos.ltb a a0 then False else ltList l2 l1 *)
          rewrite H.
(* Goal: True *)
          trivial.
  Qed.

  Definition compareST (cp1 cp2 : tST) :=
    compareList (PosSort.sort (CPToList cp1)) (PosSort.sort (CPToList cp2)).

  Lemma compare_spec : forall cp1 cp2,
    CompSpec eqST ltST cp1 cp2 (compareST cp1 cp2).
  Proof.
    intros cp1 cp2.
    unfold eqST, ltST, compareST.
    apply compareListSpec.
  Qed.
(*
TODO: try to see if using sorted lists would not make the tactic faster.
*)
  Definition STelt := tST.

  Definition STt := list tST.

  Definition STempty : STt := nil.

  Lemma eqST_dec : forall x y, {eqST x y} + {~ eqST x y}.
  Proof.
(* Goal: forall _ : and (Pos.eq a a0) (eqList l1 l2), @eq (list positive) (@cons positive a l1) (@cons positive a0 l2) *)
    intros x y; case_eq (eqbST x y); intro HEq.

(* Goal: sumbool (eqST x y) (not (eqST x y)) *)
(* Goal: sumbool (eqST x y) (not (eqST x y)) *)
      apply eqbST_eqST in HEq; left; auto.

(* Goal: sumbool (eqST x y) (not (eqST x y)) *)
      right; intro HEqST; apply eqbST_eqST in HEqST; rewrite HEq in *; discriminate.
  Qed.

  Definition STadd (x : STelt) (s : STt) := cons x s.

  Fixpoint STexists_ (f : STelt -> bool) (s : STt) :=
    match s with
      | nil      => false
      | hd :: tl => f hd || STexists_ f tl
    end.

  Fixpoint STmem elt l :=
    match l with
      | nil      => false
      | hd :: tl => if eqST_dec hd elt then true else STmem elt tl
    end.

  Lemma STempty_b : forall y : STelt, STmem y STempty = false.
  Proof. intros. reflexivity. Qed.

  Lemma STexists_mem_4 :
    forall f (s : STt),
      STexists_ f s = true ->
      exists x : STelt ,  STmem x s = true /\ f x = true.
  Proof.
    intros f s HEx; induction s;
    simpl in *; [discriminate|].
(* Goal: @ex STelt (fun x : STelt => and (@eq bool (if eqST_dec a x then true else STmem x s) true) (@eq bool (f x) true)) *)
    case_eq (f a); intro Hfa; rewrite Hfa in *; simpl in *.

      exists a; elim (eqST_dec a a);
      [intuition|intro H; exfalso; apply H; unfold eqST; apply eqListRefl].

(* Goal: @ex STelt (fun x : STelt => and (@eq bool (if eqST_dec a x then true else STmem x s) true) (@eq bool (f x) true)) *)
      destruct (IHs HEx) as [x [Hmem Hfx]]; exists x.
(* Goal: if Pos.ltb hdx hdz then True else if Pos.ltb hdz hdx then False else ltList tlx tlz *)
      elim (eqST_dec a x); intro; intuition.
  Qed.

  Lemma STadd_iff : forall (s : STt) (x y : STelt),
    STmem y (STadd x s) = true <-> (eqST x y \/ STmem y s = true).
  Proof. intros; simpl; elim (eqST_dec x y);intro;intuition. Qed.

End Set_of_tuple_of_positive.
