proposition: Theorem right_compose_fi f f': f' \coP f -> injection (f' \co f) -> injection f.
proof: Proof. move=> cff [fc ic];split; first by fct_tac. by move: ic; aw=> ic x y xs ys eql; apply: ic => //; rewrite !compfV //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)