proposition: Lemma surj_left_compose2C (a b c:Set) (f:a->b) (f':b->c): surjectiveC (f' \o f) -> injectiveC f' -> surjectiveC f.
proof: Proof. by move => sc if' x; move: (sc (f' x)) => [y sv]; exists y; apply: if'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)