proposition: Lemma right_inverse_pr (a b:Set) (f: a->b) (H:surjectiveC f) (x:b): f (right_inverseC H x) = x.
proof: Proof. by rewrite /right_inverseC; apply:(chooseT_pr (p:= fun k : a => f k = x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)