proposition: Theorem right_inv_compose_rf f f' s'': f' \coP f -> is_right_inverse (f' \co f) s'' -> is_right_inverse f' (f \co s'').
proof: Proof. move=> cff [[ fc fs]]; aw => cffsi cc. have [ff' ff seq]: (f' \coP f) by []. have cfs: f \coP s'' by hnf. by split; [saw; fct_tac | rewrite compfA ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)