proposition: Lemma zprod2_pr1 a b x: inc x (zprod2 a b) -> ((x \cap a = singleton (zpr x a)) /\ (x \cap b = singleton (zpr x b))).
proof: Proof. rewrite /zpr. by move /zprod2_P => [pa [t ->] [s ->]]; rewrite ! setU_1. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)