proposition: Lemma perm_ints n f: natp n -> surjection f -> source f = n -> target f = n -> inc f (permutations n).
proof: Proof. move => nN pb pc pd; apply/permutationsP; split => //. apply:bijective_if_same_finite_c_surj => //; first by rewrite pc pd. by rewrite pc; apply:finite_set_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)