proposition: Lemma perm_int_inj n f: natp n -> inc f (permutations n) -> (forall x y, x <c n -> y <c n -> Vf f x = Vf f y -> x = y).
proof: Proof. move => nN /permutationsP[ [[_ H] _] sf _]. rewrite sf in H. by move => x y /(NltP nN) xs /(NltP nN) ys sv; apply:H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)