proposition: Lemma ext_to_prod_inverse u v: bijection u -> bijection v-> inverse_fun (u \ftimes v) = (inverse_fun u) \ftimes (inverse_fun v).
proof: Proof. move=> bu bv. have Ha:bijection (u \ftimes v) by apply: ext_to_prod_fb. have Hb:function (inverse_fun u) by apply: bijective_inv_f. have Hc:function (inverse_fun v) by apply: bijective_inv_f. apply: function_exten; fprops; try solve [rewrite /ext_to_prod; aw;trivial]. by apply: bijective_inv_f. move=> x. rewrite /ext_to_prod ifun_s lf_target; move/setX_P=>[xp pxu qxv]. rewrite ext_to_prod_V2 //; last apply:setX_i; aw;fprops. have p1: (inc (Vf (inverse_fun u) (P x)) (source u)). by rewrite -ifun_t; Wtac; rewrite ifun_s. have p2: (inc (Vf (inverse_fun v) (Q x)) (source v)). by rewrite -ifun_t; Wtac; rewrite ifun_s. have eq: x = Vf (ext_to_prod u v) (J (Vf (inverse_fun u) (P x)) (Vf (inverse_fun v)(Q x))). rewrite ext_to_prod_V //; try fct_tac. rewrite inverse_V // inverse_V //. by rewrite {1} eq inverse_V2 // /ext_to_prod; aw;apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)