proposition: Lemma nds_max_bd_prop f: [/\ f \0c = \1c, f \1c = \1c, nds_fbd f & nds_fmax f] <-> [/\ f \0c = \1c, f \1c = \1c & nds_fixpt_eq f].
proof: Proof. split. move => ha. have fN:= (nds_bdmax_nat ha). move: ha => [f0 f1 fb fm]; split => // n nN ge2. have ln1: \1c <c n by apply/(cleSltP NS1); rewrite succ_one. set I := Zo _ _; set E := fun_image _ _. apply: cleA. have csE: cardinal_set E by move => t /funI_P [ k _ ->]; fprops. move: (fm _ nN ge2) => [k [ka kb kc]]. apply: (card_sup_ub csE); apply/funI_P; exists k => //. by apply/Zo_P; split => //; apply(NS_lt_nat kb nN). apply:(card_ub_sup (CS_nat (fN _ nN))) => x /funI_P [k /Zo_P [ka [kb kc]] ->]. exact:(fb n k nN ge2 kb kc). move => ha. suff: forall n, natp n -> \2c <=c n -> (forall k, \0c <c k -> k <c n -> ndsC k *c f (n -c k) <=c f n) /\ (exists k, [/\ \0c <c k, k <c n & ndsC k *c f (n -c k) = f n]). move: ha => [f0 f1 fre] h; split => //. by move => n k ha hb hc hd; apply:(proj1 (h n ha hb)). move => n ha hb; exact:(proj2 (h n ha hb)). move => n nN ne2. move:(proj33 ha n nN ne2). set I := Zo _ _; set E := fun_image _ _ => ->. have csE: cardinal_set E by move => t /funI_P [ k _ ->]; fprops. split. move => k lp lkn. apply:(card_sup_ub csE); apply/funI_P; exists k => //. apply/Zo_P; split => //; apply: (NS_lt_nat lkn nN). have fn:= (nds_bdmax_nat' ha). have l1n: \1c <c n by apply/(cleSltP NS1); rewrite succ_one. have EN: sub E Nat. move=> t /funI_P [k /Zo_P[ka [kb kc]] ->]; apply:(NS_prod (NS_ndsC ka)). apply(fn _ (NS_diff _ nN)). have fsE: finite_set E. have hu: sub I n by move => t /Zo_P [_ [_] /(NltP nN) ]. apply:(finite_fun_image _ (sub_finite_set hu (finite_set_nat nN))). have neE: nonempty E. apply:funI_setne; exists \1c; apply: (Zo_i NS1); split; fprops. move:(finite_subset_Nat EN fsE neE) => [m me mg]. have ->: \csup E = m. apply:cleA; last exact:(card_sup_ub csE me). apply:(card_ub_sup (CS_nat (EN _ me)) mg). by move/(funI_P):me => [k /Zo_P[kN [ka kb]] ->]; exists k. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)