proposition: Lemma disjointU2_pr0 a b x y: disjoint x y -> disjoint (a \times x) (b \times y).
proof: Proof. move=> dxy; apply: disjoint_pr. move=> u /setX_P [_ _ qx] /setX_P [_ _ qy]. apply: (nondisjoint qx qy dxy). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)