proposition: Theorem exists_unique_left_composable f g h h': function f -> surjection g -> source f = source g -> h \coP g -> h' \coP g -> h \co g = f -> h' \co g = f -> h = h'.
proof: Proof. move=> ff sg sfsg chg chg' chgf chgf'. move:(exists_right_inv_from_surj sg)=> [j jp]. rewrite (exists_left_composable_aux ff sfsg jp chg chgf). by rewrite (exists_left_composable_aux ff sfsg jp chg' chgf'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)