proposition: Lemma nds_alt_prop1 n: natp n -> \1c <c n -> exists k, [/\ \0c <c k, k <c n & nds_F n <=c ndsC k *c nds_F (n -c k)].
proof: Proof. move => nN np. have np2: \2c <=c n by rewrite - succ_one; apply/(cleSltP NS1). move: (nds_F_FA_def nN np2) => [_ [k [kp kln <-]]]. exists k; split => //. move: (nds_FA_def nN kp (proj1 kln)). move=> [pa _ _ [X [pb pc <-]]]. move:(nds_type_nor_ex nN kp (proj1 kln) pc)=> [Y [e [ ya <-]]]. rewrite /nds_card (@nds_tg9 Y n k e nN kln ya). clear pa pb pc X. set F:= (fun v1 : Set => _). set E := (nds_tn_S Y k). move:(csum_pr1_bis E F). set g1:= (Lg E (fun a => cardinal (Vg (Lg E F) a))). have <-: csum g1 = csumb E (fun a => cardinal (F a)). apply:csumb_exten => t tx; rewrite LgV //. set g2 := cst_graph E (nds_F (n -c k)). have sd: domain g1 = domain g2 by rewrite /g1/g2; aw. have kN:= NS_lt_nat kln nN. have nkN:= (NS_diff k nN). move: (nds_f_def nkN) => [pe _ pf pg]. move: ya => [[pa _] pc pd _]. suff le1:forall x, inc x (domain g1) -> Vg g1 x <=c Vg g2 x. move:(csum_increasing sd le1). rewrite [csum g2]csum_of_same cprodC - cprod2cl /E -/(nds_tn_C _ _) => ha hb. have ax: nds_tn_ax Y k. by split; [move => i ik; apply: pa (clt_ltT ik kln) | exists e]. move: (cprod_Mlele (nds_tn_max kN kp ax) (cleR (CS_nat pe))) => hc. exact:(cleT (cleT hb ha) hc). rewrite /g1 /g2; aw => a abn; rewrite !LgV//. have /pg:nds_ax(fun z => Y (k +c z)) (n -c k). move => i ink; move:(csum_Meqlt kN ink). by rewrite(cdiff_pr (proj1 kln)) => /pa /proj32_1. apply:cleT; apply:fun_image_smaller. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)