proposition: Lemma ext_map_prod_taxioms: lf_axiom (fun x => Lg I (ext_map_prod_aux x f)) (productf I src) (productf I trg).
proof: Proof. move=> x /setXf_P [pa pb pc]; apply/setXf_P; split;aww. rewrite /ext_map_prod_aux => i iI; rewrite LgV //. move : (ax iI) => [fi dfi sr]; apply: sr. by apply: inc_V_range=>//;rewrite dfi; apply: pc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)