proposition: Lemma ext_map_prod_fs I p1 p2 f: ext_map_prod_axioms I p1 p2 f -> (forall i, inc i I -> range (f i) = p2 i) -> surjection (ext_map_prod I p1 p2 f).
proof: Proof. move=> emp als; set g :=(ext_map_prod I p1 p2 f). have fg: function g by apply: ext_map_prod_f. split => //. have semp: source g = productf I p1 by rewrite /g /ext_map_prod lf_source. have temp: target g = productf I p2 by rewrite /g /ext_map_prod lf_target. rewrite semp temp; move=> y yt. have ext: (forall i, inc i I -> exists2 z, inc z (p1 i) & Vg y i = Vg (f i) z). move=> i iI; move: (emp _ iI) => [ff df sr]. move /setXf_P : yt => [fy dy ip2]; move: (ip2 _ iI). by rewrite - (als _ iI); move/(range_gP ff); rewrite df. pose pr i:= (fun z => inc z (p1 i) /\ Vg y i = Vg (f i) z). set x:= Lg I (fun i => choose (pr i)). have xp: forall i, inc i I -> pr i (Vg x i). move=> i iI; rewrite LgV//; apply: choose_pr. by move: (ext _ iI) => [s xa xb]; exists s. have ixp: (inc x (productf I p1)). apply/setXf_P; rewrite /x; split; aww; rewrite -/x. by move=> i iI; aw; move: (xp _ iI) => []. have xsq: (inc x (source g)) by ue. have iWp: (inc (Vf g x)(productf I p2)) by rewrite -temp; Wtac. ex_tac; symmetry;apply: (setXf_exten iWp yt); move=> i iI /=. by rewrite ext_map_prod_VV //;move: (xp _ iI) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)