proposition: Lemma exists_left_inv_from_injC (a b:Set) (f:a->b): inhabited a -> injectiveC f -> exists r, is_left_inverseC f r.
proof: Proof. by move=> H fi; exists (left_inverseC f H); apply: left_inverse_comp_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)