proposition: Lemma setIS A B C : A \subset B -> C :&: A \subset C :&: B.
proof: Proof. move=> sAB; apply/subsetP=> x; rewrite !inE. by case: (x \in C) => //; apply: (subsetP sAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)