proposition: Lemma compose_ext_to_prod2C (a b c a' b' c':Set) (u:b-> c)(v:a->b) (u':b'-> c')(v':a'->b'): (ext_to_prodC u u') \o (ext_to_prodC v v') =1 ext_to_prodC (u \o v)(u' \o v').
proof: Proof. move => x /=; rewrite -(prJ_recov x). move: (ext_to_prod_prop v v' (pr1C x) (pr2C x));rewrite -prJ_prop=> xx. rewrite - (R_inj xx). by apply: R_inj; rewrite -2! ext_to_prod_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)