proposition: Theorem left_compose_fs2 f f': f' \coP f-> surjection (f' \co f) -> injection f' -> surjection f.
proof: Proof. move=> cff sc [_ fi]. have [ff ff' eq] := cff. split; first by fct_tac. rewrite - eq=>y ytf. have ytc: (inc (Vf f' y) (target (f' \co f))) by aw; fprops. move: ((proj2 sc) _ ytc)=> [x]; aw => xs; rewrite compfV // => eq1. by exists x => //; apply: fi=>//; rewrite eq; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)