proposition: Theorem exists_right_inv_from_surj f: surjection f -> exists s, is_right_inverse f s.
proof: Proof. move=> [ff sf]. pose p y x := inc x (source f) /\ Vf f x = y. have ha y: inc y (target f) -> p y (choose (p y)). by move => /sf [x xa xb]; apply: choose_pr; exists x. have ax: lf_axiom (fun y => choose (p y)) (target f) (source f). by move => y /ha; case. have hb: f \coP Lf (fun y : Set => choose (p y)) (target f) (source f). by saw; apply: lf_function. exists (Lf (fun y => choose (p y)) (target f) (source f)). split => //;apply:function_exten; aw; fprops; first by fct_tac. move => y yt; rewrite idV // compfV //; last by aw. rewrite LfV//; exact:proj2 (ha _ yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)