proposition: Lemma ext_to_prod_fi u v: injection u -> injection v -> injection (u \ftimes v).
proof: Proof. move=> [fu iu] [fv iv]; split; fprops. rewrite /ext_to_prod; aw. move => x y xs ys /=; rewrite ext_to_prod_V2 // ext_to_prod_V2 //. move: xs ys => /setX_P [px pxs qxs] /setX_P [py pys qys] eq. apply: pair_exten =>//. by apply: iu=>//; apply: (pr1_def eq). by apply: iv=>//; apply: (pr2_def eq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)