proposition: Lemma setI2_P x A B: inc x (A \cap B) <-> (inc x A /\ inc x B).
proof: Proof. split => [xi | [xa xb]]; last by fprops. by split; [apply: (setI2_1 xi) | apply:(setI2_2 xi)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)