proposition: Lemma subsetIidr A B : (B \subset A :&: B) = (B \subset A).
proof: Proof. by rewrite setIC subsetIidl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)