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