proposition: Lemma nds_f_def n (f := nds_F n): natp n -> [/\ natp f, f <=c factorial n, (exists2 X, nds_ax X n & nds_card X n = f) & (forall X, nds_ax X n -> nds_card X n <=c f)].
proof: Proof. move => nN. set T := (Zo Nat(fun z => exists2 X, nds_ax X n & nds_card X n = z)). move: (NS_factorial nN) => tb. have tc: (forall i, inc i T -> i <=c (factorial n)). rewrite /T;move=> i /Zo_P [iN [X ea <-]]; exact: (nds_card_bd X nN). move: (Nat_sup_pr tb tc) => [pa pb pc pd]. have pe X: nds_ax X n -> inc (nds_card X n) T. by move => ax; apply: Zo_i;[ apply: NS_nds_card | exists X]. case:pd => h. set X := (fun z: Set => \0o). have aX: nds_ax X n by rewrite /X;move => i _ /=; apply: OS0. by empty_tac1 (nds_card X n); apply: pe. by split => //; [ move:h => /Zo_P [_] | move=> X xv; apply: pc; apply: pe]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)