proposition: Lemma exercise4_3b x y y' z: nonempty(y \cap y') -> (y' \times z) \cg (x \times y) = x \times z.
proof: Proof. move=> [t /setI2_P [ty ty']]. set_extens u. move /compg_P => [pu [v /setXp_P [pa _] /setXp_P [_ pb]]]. by apply:setX_i. move => /setX_P [pu Px Qy]; apply/compg_P; split => //; exists t; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)