proposition: Lemma nds_F_FA_def n (g := nds_FA n) (f:= nds_F n): natp n -> \2c <=c n -> (forall k, \0c <c k -> k <c n -> (g k) <=c f) /\ (exists k, [/\ \0c <c k, k <c n & (g k) = f]).
proof: Proof. move=> nN nge2. split. by move => k kp kn ; move: (nds_FA_def nN kp (proj1 kn)) => [_ pa _]. case: (equal_or_not n \2c) => en2. move: clt_12 clt_01 => ra rb. rewrite /f /g en2 nds_f2; exists \1c; split => //; exact: nds_FA_21. move: (nds_f_def nN); rewrite -/f; move=> [_ _ [X ax fv] pd]. move: (clt_leT clt_02 nge2) => np. case: (p_or_not_p (exists2 i, i<c n & X i = \0o)) => tp0. move:(nds_type0 nN nge2 ax tp0) => [y ay xsy]. by case: (cleNgt(pd y ay)); rewrite - fv. set E:= fun_image n (fun i => odegree (X i)). set m := intersection E. set F := (Zo n (fun i => odegree (X i) = m)). have s1: sub F n by apply Zo_S. move: (sub_smaller s1); rewrite (card_nat nN) => kn. have osE: ordinal_set E. rewrite /E; move=> t /funI_P [z /(NltP nN) /ax zi ->]. by apply: OS_degree. have neE: nonempty E by apply:funI_setne; exists \0c; apply/(NltP nN). move: (ordinal_setI neE osE); rewrite -/m => mE. set k := cardinal F. have kp: \0c <c k. move: mE => /funI_P [z zn zv]. apply: (card_ne0_pos (CS_cardinal _) (card_nonempty1 _)). by exists z; apply: Zo_i. have kt: nds_type X n k. split. move => i lin; case: (ozero_dichot (ax _ lin)) => //. by move => baa;case: tp0; exists i. have om: ordinalp m by apply:osE. exists m; split => // i /(NltP nN) lin. have uE: inc (odegree (X i)) E by apply /funI_P; ex_tac. by split; [ exact | apply: osE | apply:setI_s1]. have eq1: g k = f. move:(nds_FA_def nN kp kn) => [_ _ qa [Y [ax' x3 x4]]]; apply cleA. by rewrite /g - x4; apply: pd. by move: (qa _ ax kt); rewrite fv. case: (equal_or_not k n) => ekn; last by exists k. case: (cltNge (nds_sd2 nN (conj nge2 (nesym en2)))); rewrite -/f - eq1 /g ekn. move: (nds_FA_def nN np (cleR (CS_nat nN))). move => [vB vle _ [Y [ay [ty1 [m' [om mp1 mp2]]] <-]]]. have fsI:= (finite_set_nat nN). move: (cardinal_setC4 (@Zo_S n (fun i => odegree (Y i) = m')) fsI). rewrite (card_nat nN) mp2 cdiff_nn => /card_nonempty /empty_setC si. apply: (nds_card_same_deg_bd nN np ty1 (e:=m')). by move => i /(NltP nN) /si /Zo_hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)