proposition: Lemma setXp_P x y A B: inc (J x y) (A \times B) <-> (inc x A /\ inc y B).
proof: Proof. by split; [move/setX_P=> [_]; aw | move=> [xa ya]; apply: setXp_i]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)