proposition: Lemma setX_relP x y a b: related (x \times y) a b <-> (inc a x /\ inc b y).
proof: Proof. by split;[ move/setX_P => [_ ]; aw | move => [ax biy]; apply: setXp_i ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)