proposition: Theorem compose_fs f f': surjection f -> surjection f' -> f' \coP f -> surjection (f' \co f).
proof: Proof. move=> [_ sf] [_ sf'] c; split; [fct_tac | aw => y yt]. move: (sf' _ yt) => [x xs ->]. have xt: inc x (target f) by rewrite - (proj33 c). by move: (sf _ xt) => [z zs ->]; ex_tac;rewrite compfV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)