proposition: Theorem right_inverse_compose f f' s s': f' \coP f -> is_right_inverse f' s' -> is_right_inverse f s -> is_right_inverse (f' \co f) (s \co s').
proof: Proof. move=> cf'f ri1 ri2. have css':= (right_inverse_composable cf'f ri1 ri2). have sstf:= (right_i_source ri2). have tssf:=(right_i_target ri2). have sf'sr: (target f = target s') by rewrite - (proj33 css'). have [cfs' cfsi'] := ri1. have [cfs cfsi] := ri2. split. by split; [ fct_tac | fct_tac | aw;rewrite -tssf]. have crrf: f \coP (s \co s') by split; [ fct_tac | fct_tac| aw ]. rewrite - compfA=>//; rewrite (@compfA f s s')=>//. by aw; rewrite cfsi sf'sr compf_id_l=>//; fct_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)