proposition: Lemma nds_value_prop f: f 0 = 1 -> f 1 = 1 -> (forall n, 1 < n -> f n = (ndsC (nds_k_of n)) * f (n - (nds_k_of n))) -> (forall n, f n = nds_sol n).
proof: Proof. move => H0 H1 Hr. move => n; move: (leqnn n); elim: n {- 2} (n). by move => n; rewrite leqn0 => /eqP ->; rewrite H0 nds_sol0. move => n Hrec p; rewrite leq_eqVlt; case/orP; last by rewrite ltnS => /Hrec. move/eqP ->. case: (posnP n) => np; first by rewrite np H1 nds_sol1. have ng1: 1 < n.+1 by rewrite ltnS. move: (nds_k_of_bd ng1) => /andP[kp]; rewrite ltnS => cp1. move: kp; rewrite -(ltn_add2r (n - nds_k_of n.+1)) add0n (subnKC cp1) => lt2. by rewrite (Hr _ ng1) (nds_sol_with_k ng1) Hrec // (subSn cp1). Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)