proposition: Lemma nb_permutations_nat m: natp m -> cardinal (permutations m) = factorial m.
proof: Proof. move => mN; rewrite card_permutations. by rewrite (card_card(CS_nat mN)). by apply: finite_set_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)