proposition: Lemma right_inverse_composable f f' s s': f' \coP f -> is_right_inverse f' s' -> is_right_inverse f s -> s \coP s'.
proof: Proof. move=> [_ _ c] [[_ fs r1] _] ri1. move: (ri1)=> [[_ fs' _] _]. by split => //; rewrite (right_i_source ri1) -c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)