proposition: Lemma setISS A B C D : A \subset C -> B \subset D -> A :&: B \subset C :&: D.
proof: Proof. by move=> /(setSI B) /subset_trans sAC /(setIS C) /sAC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)