proposition: Lemma left_inverse_surjectiveC (a b:Set) (r:b->a)(f:a->b): is_left_inverseC f r -> surjectiveC r.
proof: Proof. by move=> h; apply: surj_if_exists_right_invC; exists f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)