proposition: Lemma inverse_ext_to_prod2C (a b a' b':Set) (u:a->a')(v:b->b') (Hu: bijectiveC u)(Hv:bijectiveC v): inverseC (bijective_ext_to_prod2C Hu Hv) =1 ext_to_prodC (inverseC Hu)(inverseC Hv).
proof: Proof. move => x. suff ww: x = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) x). by rewrite ww inverseC_pra -ww. move: (compose_ext_to_prod2C u (inverseC Hu) v (inverseC Hv))=> eq. move: (eq x) => /= ->. rewrite - (prJ_recov x); apply: R_inj. by rewrite -ext_to_prod_prop /= inverseC_prb inverseC_prb prJ_prop. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)