proposition: Lemma left_inv_compose_rf2C (a b c:Set) (f:a->b) (f':b->c)(r'': c->a): is_left_inverseC (f' \o f) r'' -> surjectiveC f -> is_left_inverseC f' (f \o r'').
proof: Proof. move=> li s t;move: (s t) => [v <-]; exact: (f_equal f (li v)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)