proposition: Theorem exists_left_composable_aux f g s h: function f -> source f = source g -> is_right_inverse g s -> h \coP g -> h \co g = f -> h = f \co s.
proof: Proof. move=> gg sfsg [csg cshi] chg <-. have shtg:(source h= target g) by move: chg=> [_ _]. by rewrite - compfA // cshi - shtg compf_id_r //; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)