proposition: Theorem left_compose_fi2 f f': f' \coP f -> injection (f' \co f) -> surjection f -> injection f'.
proof: Proof. move=> cff [_ ic] sf. split; first by fct_tac. rewrite (proj33 cff) => x y xs ys. have [x' x's e1] := ((proj2 sf) _ xs). have [y' y's e2] :=((proj2 sf) _ ys). rewrite compf_s in ic; move: (ic _ _ x's y's). by rewrite !compfV // e1 e2 => e3 e4; rewrite (e3 e4). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)