proposition: Lemma properI2_r A B : ~(sub B A) <-> ssub (A \cap B) B.
proof: Proof. split; first by move => nba; split;[ apply:subsetI2r | move /setI2id_Pr]. by move =>[_ hb] /setI2id_Pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)