proposition: Lemma Sprod_P A B x: inc x (Sprod A B) <-> exists a1 b1 a2 b2, [/\ inc (J a1 a2) A, inc (J b1 b2) B & x = J (J a1 b1) (J a2 b2)].
proof: Proof. split. move => /Zo_P. set a := P (P x); set b := P (Q x); set c := Q (P x); set d := Q (Q x). move => [h1 [h2 h3]]; exists a,c,b,d; split => //. move/setX_P: h1 => [r1 /setX_P[r2 _ _] /setX_P [r3 _ _]]. by rewrite - r1 -r2 - r3. move => [a1 [a2 [b1 [b2 [ha hb ->]]]]]. apply:Zo_i; last by aw. apply: setXp_i; apply:setXp_i; apply/funI_P. - by exists (J a1 b1); aw. - by exists (J a2 b2); aw. - by exists (J a1 b1); aw. - by exists (J a2 b2); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)