proposition: Lemma exists_left_composableC (a b c:Set) (f:a->b)(g:a->c): surjectiveC g -> ((exists h, h \o g =1 f) <-> (forall (x y:a), g x = g y -> f x = f y)).
proof: Proof. move=> sg; split. by move=> [h hp] x y; move: (hp x) (hp y) => /= <- <- <-. move: (exists_right_inv_from_surjC sg) => [h hp] hyp. by exists (f \o h) => t /=; apply: hyp; move:(hp (g t)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)