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