proposition: Theorem exists_right_composable_aux f g h r: function f -> target f = target g -> is_left_inverse g r -> g \coP h -> g \co h = f -> h = r \co f.
proof: Proof. move=> ff tftg [crg crgi] chg <-; rewrite compfA // crgi. by move:chg=> [_ fh ->];rewrite compf_id_l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)