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