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