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