proposition: Lemma nds_bdmax_nat f: [/\ f \0c = \1c, f \1c = \1c, nds_fbd f & nds_fmax f] -> forall n, natp n -> natp (f n).
proof: Proof. move => [f0 f1 _ fm]; 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. move:(fm (csucc n) nsN np2) => [k [/proj2/nesym ka kb <-]]; apply: NS_prod. apply:(NS_ndsC (NS_lt_nat kb nsN)). apply: Hr; apply/(cltSleP nN); apply:(cdiff_ltb nsN (proj1 kb) ka). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)