proposition: Lemma zprod2_P a b y: inc y (zprod2 a b) <-> [/\ sub y (a \cup b), singletonp (y \cap a) & singletonp (y \cap b)].
proof: Proof. split. move => /Zo_P [] /setP_P pa pb;split => //; apply: pb; fprops. move => [pa pb pc]; apply /Zo_P; split; first by apply /setP_P. by move => x /set2_P; case => ->. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)