proposition: Lemma zprod2_pr2 a b x: inc x (zprod2 a b) -> x = doubleton (zpr x a) (zpr x b).
proof: Proof. move=> yz; set_extens z; aw. move: (yz) => /zprod2_P [pa pb pc]. move=> xy; move: (pa _ xy);case /setU2_P => h. rewrite (zprod2_pr1a yz h xy); fprops. rewrite (zprod2_pr1b yz h xy); fprops. by move: (zprod2_pr0ax yz) (zprod2_pr0bx yz) => pa pb;case /set2_P=> ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)