proposition: Lemma nds_alt (f: nat -> nat) (c:= ndsC) : f 0 = 1 -> f 1 = 1 -> (forall n, 2 <= n -> exists2 k, 0 < k < n & f n <= (c k) * (f (n - k))) -> (forall n, nds_sol n.+1 <= f n.+1) -> (forall n, nds_sol n = f n).
proof: Proof. move => HF0 HF1 HFle HFge. move => n; move: (leqnn n); elim: n {- 2} (n). by move => n; rewrite leqn0 => /eqP ->; rewrite nds_sol0 HF0. move => n Hr p; rewrite leq_eqVlt; case/orP; last by rewrite ltnS => /Hr. move/eqP ->. apply: anti_leq; rewrite HFge. case:(posnP n); first by move ->; rewrite nds_sol1 HF1. rewrite - ltnS;move => np. move: (HFle _ np) => [k klt kv]; apply: (leq_trans kv). move: (@nds_sol_bd _ _ np klt). move/andP: klt => [kp ]; rewrite ltnS => kn1. by rewrite (subSn kn1) - Hr // - (subSn kn1) leq_subLR -{1}(add0n n) ltn_add2r. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)