proposition: Theorem exists_left_inv_from_inj f: injection f -> nonempty (source f) -> exists r, is_left_inverse f r.
proof: Proof. move=> fi [a asf]; move: (inj_function fi) => ff. pose p x y := x = Vf f y. pose gx x := (select (p x) (source f)). have hc x: inc x (Imf f) -> p x (gx x) /\ inc (gx x) (source f). move => xI; apply: select_pr; first by move/(Imf_P ff): xI. rewrite /p; move => i j /= isf e1 jsf e2;apply: (proj2 fi i j isf jsf). by rewrite - e1 e2. pose g x := Yo (inc x (Imf f)) (gx x) a. have ax: lf_axiom g (target f) (source f). rewrite /g => t tt; Ytac h => //; exact:(proj2 (hc _ h)). have ha: Lf g (target f) (source f) \coP f. by saw; apply:lf_function. exists (Lf g (target f) (source f)). split => //; apply: function_exten; aw; fprops; first by fct_tac. move => y ys /=. have yi:inc (Vf f y) (Imf f) by apply/(Imf_P ff); ex_tac. have ft: inc (Vf f y) (target f) by Wtac. move: (hc _ yi) => [hu hv]; move:(proj2 fi _ _ ys hv hu) => yv. by rewrite LfV // compfV // LfV // /g; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)