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