proposition: Lemma nds_FA_def n k (v := nds_FA n k): natp n -> \0c <c k -> k <=c n -> [/\ natp v, v <=c (nds_F n), (forall X, nds_ax X n -> nds_type X n k -> nds_card X n <=c v) & (exists X, [/\ nds_ax X n, nds_type X n k & nds_card X n = v])].
proof: Proof. move=> nN kp kn. rewrite /v /nds_FA; set T:= Zo Nat _. have tb: natp (nds_F n) by move: (nds_f_def nN) => [ok _]. have tc: (forall i, inc i T -> i <=c (nds_F n)). move => i /Zo_P [_ [X [ax <- _]]]. by move: (nds_f_def nN) => [_ _ _ p4]; apply: p4. move: (Nat_sup_pr tb tc) => [pa pb pc pd]. have pe X: nds_ax X n -> nds_type X n k -> inc (nds_card X n) T. by move => ax ax2; apply: Zo_i;[ apply: NS_nds_card | exists X]. split => //. by move=> X ax ax2; apply: pc; apply: pe. case: pd; last by move /Zo_P=> [_ [X [p1 p2 p3]]];exists X; split. move: (nds_type_exists_bd nN kp kn)=> [X [ax tx]] te. empty_tac1 (nds_card X n);apply:pe. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)