proposition: Lemma nds_tn_ex_val n: natp n -> nds_tn_C nds_base n = ndsC n.
proof: Proof. move => nN. have ha: forall i, natp i -> natp (\2c ^c i). move => i; apply:(NS_pow NS2). rewrite /nds_tn_C (nds_tnmax_ex nN). have sk2_S a K: inc K (\Po (n -s1 a)) -> sumpow2 (K +s1 a) = sumpow2 K +c \2c ^c a. move => /setP_P KS. by rewrite /sumpow2 (csumA_setU1) // => /KS /setC1_P []. have sk2_N a K: inc a n -> inc K (\Po (n -s1 a)) -> natp (sumpow2 (K +s1 a)). move => aN KP. rewrite (sk2_S a K KP); apply:(NS_sum (sumpow2_N2 nN KP)). exact:(NS_pow NS2 (NS_inc_nat nN aN)). rewrite csucc_pr; last first. move/setUf_P => [a an /funI_P [K Ka]]; apply/nesym. have aN := (NS_inc_nat nN an). move:(OS_nat (sk2_N _ _ an Ka)) => o1. move/(osum2_zero (OS_prod2 OS_omega o1) (OS_nat aN)) => /proj1. apply:(oprod2_nz OS_omega o1 omega_nz); rewrite (sk2_S _ _ Ka) => /csum_nz. by move => [_] /cpow2_nz. rewrite /ndsC; congr csucc;rewrite csum_pr4_bis; last first. move => i j iN jN; case (equal_or_not i j) => eij; [by left | right]. apply:disjoint_pr => u /funI_P [K1 K1p uv1] /funI_P [K2 K2p uv2]; case eij. rewrite uv1 in uv2. move: (sk2_N _ _ iN K1p) (sk2_N _ _ jN K2p) => e2 e4. by case: (omega_monom_inj e2 (NS_inc_nat nN iN) e4 (NS_inc_nat nN jN) uv2). set F := fun a:Set => _. suff H: forall a, inc a n -> F a = \2c ^c cpred n. rewrite - {2} (card_nat nN) (cprod2cl). by rewrite cprodC - csum_of_same; apply: csumb_exten => i ib /=; apply: H. move => a an; rewrite - (nds_C_prop nN an) /F cardinal_fun_image //. move => K1 K2 K1a K2a /= eq1. move:(sk2_N _ _ an K1a) (sk2_N _ _ an K2a) => s1N s2N. have aN := (NS_inc_nat nN an). move: (proj1 (omega_monom_inj s1N aN s2N aN eq1)). rewrite (sk2_S _ _ K1a) (sk2_S _ _ K2a) => eq2. move:(csum_eq2r (NS_pow NS2 aN) (sumpow2_N2 nN K1a) (sumpow2_N2 nN K2a) eq2). apply: (sumpow2_inj nN) => i. by move/setP_P: K1a => h; move=> /h /setC1_P /proj1/(NltP nN). by move/setP_P: K2a => h; move=> /h /setC1_P /proj1/(NltP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)