proposition: Lemma nds_tn_max X n: natp n -> \0c <c n -> nds_tn_ax X n -> nds_tn_C X n <=c ndsC n.
proof: Proof. move => nN np ax. rewrite /ndsC /nds_tn_C (nds_tn_prop2 nN np ax); set F:= (fun a : Set => _). suff h: cardinal (unionf n F) <=c (n *c \2c ^c cpred n). have w:cardinalp (n *c \2c ^c cpred n) by fprops. case: (inc_or_not \0c (unionf n F)) => ha. rewrite (setU1_eq ha); apply:(cleT h (cleS0 w)). by rewrite (csucc_pr ha); apply /(cleSSP (CS_cardinal _) w). apply: (cleT(csum_pr1_bis n F));rewrite cprodC - csum_of_same. apply:csum_increasing; aw; trivial => a abn; rewrite !LgV//. rewrite - (nds_C_prop nN abn); apply:fun_image_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)