proposition: Lemma exercise4_3a x y y' z: disjoint y y' -> (y' \times z) \cg (x \times y) = emptyset.
proof: Proof. rewrite /disjoint => ie; apply /set0_P. move=> t => /compg_P [_ [u /setXp_P [_ uy] /setXp_P [uy' _]]]. by empty_tac1 u. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)