proposition: Lemma setI2_SS A B C D : sub A C -> sub B D -> sub (A \cap B) (C \cap D).
proof: Proof. move => s1 s2; apply: sub_trans (setI2_S1 (C:=C) s2); apply: (setI2_S2 s1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)