proposition: Lemma ext_map_prod_fi I p1 p2 f: ext_map_prod_axioms I p1 p2 f -> (forall i, inc i I -> injective_graph (f i)) -> injection (ext_map_prod I p1 p2 f).
proof: Proof. move=> emp alli; split; first by apply: ext_map_prod_f. rewrite /ext_map_prod lf_source => x y xp yp eql. apply: (setXf_exten xp yp) =>i iI. move: (ext_map_prod_VV emp xp iI); move: (ext_map_prod_VV emp yp iI). rewrite eql; move=> -> aux. move: (emp _ iI)=> [_ df sr]. move: (alli _ iI) => [ff]; apply =>//; rewrite df. by move: xp=> /setXf_P [_ dx]; apply. by move /setXf_P: yp => [_ dx]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)