proposition: Lemma ext_map_prod_composable I p1 p2 p3 g f h: ext_map_prod_axioms I p1 p2 f -> ext_map_prod_axioms I p2 p3 g -> (forall i, inc i I -> h i = (g i) \cf (f i)) -> (forall i, inc i I -> (g i) \cfP (f i)) -> ext_map_prod_axioms I p1 p3 h.
proof: Proof. move=> emp1 emp2 alh alfc x xs. move: (emp1 _ xs) (emp2 _ xs) => [fgg dg srg] [fgf df srf]. move: (alfc _ xs)(alh _ xs) => fca ->. have fgc: fgraph ((g x) \cf (f x)) by apply: composef_fgraph. have dfc :domain((g x) \cf (f x)) = domain (f x) by rewrite /composef; aw. rewrite dfc dg; split=>//. move=> y /(range_gP fgc) [z zdg ->];rewrite composef_ev //; last by ue. apply: srf; apply/(range_gP fgf); exists (Vg (f x) z) => //. rewrite df; apply: srg; apply: inc_V_range =>//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)