proposition: Lemma nds_tn_def n (f:= nds_tn_sup n): natp n -> [/\ natp f, \0c <c f, (exists2 X, nds_tn_ax X n & nds_tn_C X n = f) & (forall X, nds_tn_ax X n -> nds_tn_C X n <=c f)].
proof: Proof. move => nN. rewrite /f /nds_tn_sup; set T := Zo _ _. have kN:=(NS_prod (NS_pow NS2 nN) (NS_factorial nN)). set k := \2c ^c n *c factorial n. have H: forall X, nds_tn_ax X n -> nds_tn_C X n <=c k. by move => X [ax _]; apply:(nds_tn_small nN) => i /ax /proj32_1. have H1:forall X, nds_tn_ax X n -> natp (nds_tn_C X n). move => X x1; exact:(NS_le_nat (H _ x1) kN). have ks:forall i, inc i T -> i <=c k by move => z /Zo_hi [X /H ax <-]. pose X (i:Set):= \1o. have ax: nds_tn_ax X n. split; first by move => i _; exact olt_01. by exists \0o; [ apply:OS0 | move=> i _; rewrite odegree_one]. have ta: inc (nds_tn_C X n) T by apply: (Zo_i (H1 _ ax)); exists X. have ha: \0c <c union T. have: nonempty (nds_tn_S X n). have idp:=(permutation_id n). exists (nds_sc (fun z => X (nth_elt n z)) (cardinal n) (identity n)). apply/setUf_P; exists n; first by apply:setP_Ti. rewrite /nds_sc_Ktau (card_nat nN);apply/funI_P;ex_tac. move /card_nonempty1; rewrite -/(nds_tn_C X n) => h0. have cst:cardinal_set T by move => t /Zo_S /CS_nat. exact:(clt_leT (card_ne0_pos (cst _ ta) h0) (card_sup_ub cst ta)). move: (Nat_sup_pr kN ks) => [pa pb pc pd];split => //; last first. move => Y x1; apply: pc; apply/ Zo_P; split; [by apply: H1 | by exists Y]. by case:pd => h1; [ empty_tac1 (nds_tn_C X n) | exact: (Zo_hi h1)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)