proposition: Lemma left_inv_compose_rfC (a b c:Set) (f:a->b) (f':b->c)(r'': c->a): is_left_inverseC (f' \o f) r'' -> is_left_inverseC f (r'' \o f') .
proof: Proof. by move=> li x; apply: (left_i_v x li). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)