proposition: Lemma left_inverseC_pr (a b:Set) (f: a->b) (H:inhabited a) (u:a): f (left_inverseC f H (f u)) = f u.
proof: Proof. rewrite /left_inverseC. set p:= fun u:a => _. have: (p (chooseT p H)) by apply: chooseT_pr; exists u; right. by case=>//; case; exists u. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)