proposition: Theorem left_compose_fs f f': f' \coP f -> surjection (f' \co f) -> surjection f'.
proof: Proof. move=> cff sc; split; first by fct_tac. have: (target f' = target (f' \co f)) by aw. move=> -> y yt; move: ((proj2 sc) _ yt)=> [x xs ->]. rewrite compf_s in xs; exists (Vf f x); last by apply compfV. move:cff=> [_ ff ->]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)