proposition: Lemma subsetI2_P A B C : sub C (A\cap B) <-> (sub C A /\ sub C B).
proof: Proof. split; last by move => [h1 h2]; apply: setI2_12S. move => h;split; apply: (sub_trans h); [apply: subsetI2l |apply: subsetI2r]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)