proposition: Theorem InEqOlistInv : forall (a b : A) (L1 L2 : list A), InclEq (a :: L1) (b :: L2) -> Olist (a :: L1) -> Olist (b :: L2) -> InclEq (a :: L1) L2 \/ eqA a b /\ InclEq L1 L2.
proof: Proof. intros a b L1 L2 H' H'0 H'1. case (ltADec a b); intros Eqab. Casec Eqab; intros Eqab. absurd (Olist (a :: b :: L2)); auto. apply InEqNList; auto. inversion H'; auto. left. inversion H'; auto. apply InclEqDef; auto. intros a0 H'2. lapply (H a0); [ intros H'4 | idtac ]; auto. inversion H'4; auto. absurd (Olist (a0 :: a :: L1)); auto. apply InEqNList; auto. apply OlistCons; auto. apply ltAeqAComp with (a := b) (b := a); auto. right; split; auto. apply InclEqDef; auto. intros a0 H'2. inversion H'. lapply (H a0); [ intros H'4 | idtac ]; auto. inversion H'4; auto. absurd (eqA a a0); auto. apply ltAImpNotEqA; auto. apply InEqSup with (L := L1); auto. apply eqATrans with (y := b); auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)