proposition: Lemma ext_to_prod_fs u v: surjection u -> surjection v -> surjection (u \ftimes v).
proof: Proof. move=> [fu su] [fv sv]. split; first by fprops. move=> y; rewrite ext_to_prod_s /ext_to_prod; aw. move/setX_P=> [py ptu qtv]. move: (su _ ptu)=> [pv prv prw]. move: (sv _ qtv)=> [qv qrv qrw]. exists (J pv qv); fprops. by rewrite ext_to_prod_V // - prw - qrw py. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)