proposition: Lemma injective_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b'): injectiveC u -> injectiveC v -> injectiveC (ext_to_prodC u v).
proof: Proof. move=> iu iv x x' / (congr1 (@Ro (product a' b'))). rewrite -(prJ_recov x) -(prJ_recov x'). rewrite - 2!ext_to_prod_prop; move=> eql. by rewrite (iu _ _ (R_inj (pr1_def eql))) (iv _ _ (R_inj (pr2_def eql))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)