proposition: Lemma right_inverse_comp_id (a b:Set) (f:a-> b) (H:surjectiveC f): f \o (right_inverseC H) =1 @id b.
proof: Proof. move=> x; rewrite composeC_ev;apply: right_inverse_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)