proposition: Lemma ext_to_prod_r: Imf (u \ftimes v) = (Imf u) \times (Imf v).
proof: Proof. have fe: (function (u \ftimes v)) by apply:ext_to_prod_f. set_extens t. move/(Imf_P fe) => [x ]; rewrite (ext_to_prod_s) => xs ->. rewrite (ext_to_prod_V2 xs); move/setX_P:xs => [_ px qx]. apply /setXp_i; Wtac. move/setX_P => [pt /(Imf_P fu) [x xsu xp] /(Imf_P fv) [y ysv yp]]. apply/(Imf_P fe);rewrite ext_to_prod_s; exists (J x y);first by fprops. by rewrite (ext_to_prod_V)// - pt xp yp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)