proposition: Lemma factorize_range (A B C : Type) (f : B -> C) (g : A -> C) : (range g `<=` range f)%classic -> exists h : A -> B, g = f \o h.
proof: Proof. move=> gf; have [h gfh] : {h & forall a, g a = f (h a)}. apply: (@choice _ _ (fun a b => g a = f b)) => a. have /cid2[b _ <-] : range f (g a) by apply gf; exists a. by exists b. by exists h; apply/funext => a; rewrite gfh. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist