proposition: Lemma zprod2_pr0 a b x: inc x (zprod2 a b) -> [/\ inc (zpr x a) a, inc (zpr x b) b, inc (zpr x a) x & inc (zpr x b) x].
proof: Proof. move=> xz; move: (zprod2_pr1 xz) => [pa pb]. have /setI2_P [sa sb] : (inc (zpr x a) (x \cap a)) by rewrite pa; fprops. have /setI2_P [sc sd] //: (inc (zpr x b) (x \cap b)) by rewrite pb; fprops. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)