proposition: Lemma prC_prop (a b:Set) (x: a \times b): Ro x = J (Ro (pr1C x)) (Ro (pr2C x)).
proof: Proof. have: (inc (Ro x) (a \times b)) by apply: R_inc. by rewrite /pr1C/pr2C B_eq B_eq; move/setX_P=> [-> _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)