proposition: Lemma right_inv_compose_rf2C (a b c:Set) (f:a->b) (f':b->c)(s'': c->a): is_right_inverseC (f' \o f) s'' -> injectiveC f'-> is_right_inverseC f (s'' \o f').
proof: Proof. move=> ri inj;move=> t; apply: inj; exact (ri (f' t)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)