proposition: Lemma right_inv_compose_rfC (a b c:Set) (f:a->b) (f':b->c)(s'': c->a): is_right_inverseC (f' \o f) s'' -> is_right_inverseC f' (f \o s'').
proof: Proof. move=> ri x; by apply: (right_i_v x ri). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)