fact: Definition right_inverseC (a b:Set) (f: a->b) (H:surjectiveC f) (v:b) := (chooseT (fun k:a => f k = v) match H v with | ex_intro x _ => inhabits x end).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)