proposition: Theorem DisjointInclR : forall L1 L2 L3 : list A, Disjoint L1 L2 -> InclEq L3 L2 -> Disjoint L1 L3.
proof: Proof. intros L1 L2 L3 H' H'0. apply DisjointCom. apply DisjointInclL with (L1 := L2); auto. apply DisjointCom; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)