proposition: Lemma nds_bdmax_nat' f: [/\ f \0c = \1c, f \1c = \1c & nds_fixpt_eq f] -> forall n, natp n -> natp (f n).
proof: Proof. move => [f0 f1 fe]; move => n nN; move:(cleR (CS_nat nN)). move:n nN {1 3}n; apply: Nat_induction. move => n /cle0 ->; rewrite f0; apply: NS1. move => n nN Hr p /cle_eqVlt; case; last first. move/(cltSleP nN); apply: Hr. move ->; case: (czero_dichot (CS_nat nN)). move ->; rewrite succ_zero f1; apply:NS1. move => /cge1P np. move:(NS_succ nN) => nsN. have np2: \2c <=c csucc n by rewrite - succ_one; apply/cleSS. rewrite (fe _ nsN np2). set I := Zo _ _; set E := fun_image _ _. have EN: sub E Nat. move=> t /funI_P [k /Zo_P[ka [kb kc]] ->]; apply:(NS_prod (NS_ndsC ka)). apply: Hr;apply/(cltSleP nN); apply:(cdiff_ltb nsN (proj1 kc)). exact: (nesym (proj2 kb)). have fsE: finite_set E. have hu: sub I (csucc n) by move => t /Zo_P [_ [_] /(NltP nsN) ]. apply:(finite_fun_image _ (sub_finite_set hu (finite_set_nat nsN))). have neE: nonempty E. apply:funI_setne; exists \1c; apply: (Zo_i NS1); split; fprops. by apply/cltSleP. move:(finite_subset_Nat EN fsE neE) => [m /EN me mg]. exact:(NS_le_nat (card_ub_sup (CS_nat me) mg) me). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)