proposition: Lemma exists_unique_left_composableC (a b c:Set) (f:a->b)(g:a->c) h h': surjectiveC g -> h \o g =1 f -> h' \o g =1 f -> h =1 h'.
proof: Proof. move=> sg chg chg' x. move: (exists_right_inv_from_surjC sg) => [j jp]. rewrite (exists_left_composable_auxC jp chg). by rewrite (exists_left_composable_auxC jp chg'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)