proposition: Lemma surjective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'): surjectiveC u -> surjectiveC v-> surjectiveC (ext_to_prodC u v).
proof: Proof. move=> su sv x; rewrite -(prJ_recov x). have pRx: pairp (Ro x) by case /setX_P: (R_inc x). move: (su (pr1C x)) => [y yp]; move: (sv (pr2C x)) => [y' y'p]. exists (pairC y y'); apply: R_inj. by rewrite - ext_to_prod_prop yp y'p prJ_recov pr1C_prop pr2C_prop; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)