proposition: Lemma nds_tnmax_ex n: natp n -> (nds_tn_S nds_base n) = unionf n (fun a => fun_image (\Po (n -s1 a)) (fun K => omega0 *o (sumpow2 (K +s1 a)) +o a)) +s1 \0c.
proof: Proof. move => nN. have npr:=(NS_inc_nat nN). case: (czero_dichot (CS_nat nN)) => np. rewrite /nds_tn_S np setP_0 setUf_0 set0_U2 setUf_1 cardinal_set0. apply: set1_pr1. apply: funI_setne; move: (permutation_id \0c) => h; ex_tac. move => i /funI_P [z zz ->]. by rewrite /nds_sc_Ktau /nds_sc cardinal_set0 osum_f0. rewrite (nds_tn_prop2 nN np (nds_tn_ex_ax nN)). f_equal; apply: setUf_exten => a /npr an; apply: funI_exten => K KP. rewrite (proj33 (nds_base_prop an)) (proj31 (nds_base_prop NS0)). rewrite oopow1; apply: f_equal2; [apply: f_equal | exact]. apply: csumb_exten => t tK; apply: (proj32 (nds_base_prop _)). move/setP_P: KP => KP. by case/setU1_P: tK; [ move/KP => /setC1_P [/npr] | move->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)