proposition: Lemma perm_int_surj n f: natp n -> inc f (permutations n) -> forall y, y <c n -> exists2 x, x <c n & Vf f x = y.
proof: Proof. move => nN /permutationsP[ [_ [_ H]] sf tf]. rewrite sf tf in H. by move => y /(NltP nN) /H [x /(NltP nN) sa sb]; exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)