proposition: Theorem left_inv_compose_rf2 f f' r'': f' \coP f -> is_left_inverse (f' \co f) r'' -> surjection f -> is_left_inverse f' (f \co r'').
proof: Proof. move=> cff lic sf. have bf: (bijection f). split=>//. have: (injection (f' \co f)) by apply: inj_if_exists_left_inv; exists r''. by apply: (right_compose_fi cff). move: (left_i_target lic); aw=> trsf; move:lic=> [crrf]; aw=> crrfi. have cfr: f \coP r'' by hnf;split; try fct_tac; symmetry. have fcfr:(function (f \co r'')) by fct_tac. split; first by hnf; split; try fct_tac; move: crrf=> [_ _]; aw. set (invf:= inverse_fun f). have sfti: (source f = target invf) by rewrite /invf; aw. have fi:(function invf) by apply: bijective_inv_f. have cffi: (f' \co f) \coP invf by hnf; aw; split; try fct_tac. have co3: r'' \coP ((f' \co f) \co inverse_fun f). by hnf; split;try fct_tac;move: crrf=> [_ _]; aw. have co4: r'' \coP f' by hnf; split; try fct_tac;move: crrf=> [_ _]; aw. rewrite - (compfA cfr co4) -{1} (compf_rK bf cff) (compfA crrf cffi). by rewrite crrfi sfti compf_id_l // /invf (proj33 cff) bij_right_inverse. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)