proposition: Lemma nds_card_bd X n: natp n -> nds_card X n <=c (factorial n).
proof: Proof. move=> nN. rewrite -{2} (card_nat nN) -(card_permutations (finite_set_nat nN)). apply: fun_image_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)