proposition: Theorem right_inv_compose_rf2 f f' s'': f' \coP f -> is_right_inverse (f' \co f) s'' -> injection f' -> is_right_inverse f (s'' \co f').
proof: Proof. move=> cff risc fi. have sc: (surjection (f' \co f)) by apply:surj_if_exists_right_inv; exists s''. have bf': (bijection f') by split=>//; apply: (left_compose_fs cff sc). move: (right_i_source risc); aw=> sstf. move: risc=> []; aw => cffs cffsi. have csf: (s'' \coP f') by hnf; split; try fct_tac. have fcsf: function (s'' \co f') by fct_tac. have cfc: f \coP (s'' \co f') by hnf; split; try fct_tac; move:cffs=> [_ _]; aw. have bif:= (bijective_inv_f bf'). have sf'tf: source f' = target f by move: cff=> [_ _]. set (invf:= inverse_fun f'). have cic: composable invf (f' \co f) by split; try fct_tac; rewrite/invf; aw. have cffsf: (f' \co f) \coP (s'' \co f'). hnf; split;[ fct_tac | done | by move:cfc=> [_ _]; aw ]. have ff: function f' by fct_tac. split=>//. rewrite - {1} (compf_lK bf' cff) - compfA // (compfA cffs csf). by rewrite cffsi compf_id_l // (bij_left_inverse bf') sf'tf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)