proposition: Theorem compose_fi f f': injection f -> injection f' -> f' \coP f -> injection (f' \co f).
proof: Proof. move=> [_ fi] [_ fi'] c; split; first by fct_tac. aw => x y xs ys; rewrite !compfV // =>p; apply: (fi _ _ xs ys). move:c => [_ ff c]; apply: fi' => //; rewrite c; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)