proposition: Lemma setXS (A1 B1 : {set aT}) (A2 B2 : {set aT2}) : A1 \subset B1 -> A2 \subset B2 -> setX A1 A2 \subset setX B1 B2.
proof: Proof. by move=> sAB1 sAB2; rewrite -!imset2_pair imset2S. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)