proposition: Lemma nds_tn_small X n: natp n -> nds_ax X n -> nds_tn_C X n <=c (\2c ^c n) *c (factorial n).
proof: Proof. move => nN ax. rewrite /nds_tn_C /nds_tn_S; set F:= (fun K : Set => _). apply: (cleT (csum_pr1_bis (\Po n) F)). rewrite - card_setP cprod2cl cprodC - csum_of_same. apply:csum_increasing; aw; trivial => K KN;rewrite !LgV//. move/setP_P:KN => KN. move:(sub_smaller KN); rewrite (card_nat nN) => ka. have nKN:=(NS_le_nat ka nN). apply: cleT (factorial_monotone nN ka). have pa: finite_set (cardinal K) by apply/NatP; rewrite double_cardinal. rewrite - (double_cardinal K) -(card_permutations pa). by apply:fun_image_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)