proposition: Theorem exists_left_composable f g: function f -> surjection g -> source f = source g -> ((exists h, h \coP g /\ h \co g = f) <-> (forall x y, inc x (source g) -> inc y (source g) -> Vf g x = Vf g y -> Vf f x = Vf f y)).
proof: Proof. move=> ff sg sfsg; split. by move=> [h [chg]] <- x y xs ys; rewrite !compfV // => ->. move:(exists_right_inv_from_surj sg) => [h [ha hb]] hc. move: ha => [fg fh sgth]. have ra: f \coP h by split => //; rewrite sfsg. have rb: function (f \co h) by apply:compf_f. have rc: source h = target g by move: (f_equal source hb); aw. have rd: (f \co h) \coP g by split; aw. have re: g \coP h by split. exists (f \co h); split => //. symmetry; apply: function_exten; aw;trivial; first by apply:compf_f. move => x xsf /=. have xsg: inc x (source g) by ue. have gxsh: inc (Vf g x) (source h) by rewrite rc; Wtac. have hgxsg: inc (Vf h (Vf g x)) (source g) by rewrite sgth; Wtac. rewrite!compfV //; apply: (hc _ _ xsg hgxsg). move: (f_equal (Vf ^~ (Vf g x)) hb). rewrite compfV // idV //; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)