proposition: Lemma exists_right_inv_from_surjC (a b:Set)(f:a-> b) (H:surjectiveC f): exists s, is_right_inverseC f s.
proof: Proof. exists (right_inverseC H); apply: right_inverse_comp_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)