proposition: Lemma nds_k_of_prop f: f \0c = \1c -> f \1c = \1c -> (forall n, natp n -> \1c <c n -> f n = ndsC (nds_k_of n) *c f (n -c nds_k_of n)) -> forall n, natp n -> f n = nds_sol n.
proof: Proof. move => f0 f1 hb. have hc: forall n, natp n -> natp (f n). move => n nN; move: {1 3}(n) (cleR (CS_nat nN)); move: n nN. apply:Nat_induction. move => n /cle0 ->; rewrite f0; apply: NS1. move => n nN Hr p; move/cle_eqVlt; case; last first. move/(cltSleP nN); apply: Hr. move ->; case: (czero_dichot (CS_nat nN)) => nz. rewrite nz succ_zero f1; apply: NS1. have sn1: \1c <c csucc n by rewrite - succ_zero; apply/cltSS. have snN := NS_succ nN. move:(nds_k_of_bd snN sn1) => [qa qb]. have kN:=(NS_lt_nat qb snN). rewrite(hb _ snN sn1); apply: (NS_prod (NS_ndsC kN)). move:(cdiff_ltb snN (proj1 qb) (nesym (proj2 qa))) => /(cltSleP nN) le1. exact: (Hr _ le1). pose g n := B_to_nat (f (nat_to_B n)). have hd n: f (nat_to_B n) = nat_to_B(g n). by rewrite /g (B_to_nat_pa (hc _ (nat_to_B_Nat n))). have g1: g 1 = 1 by rewrite /g /= succ_zero f1 - nat_to_B1 B_to_nat_pb. have g0: g 0 = 1 by rewrite /g /= f0 - nat_to_B1 B_to_nat_pb. have gn: forall n, 1 < n -> g n = Nds.ndsC (Nds.nds_k_of n) * g (n - Nds.nds_k_of n). move => n ln1; rewrite /g. move: (Nds.nds_k_of_bd ln1) => /andP [he hf]. move/nat_to_B_gt1:(ln1) => ln2. rewrite (hb (nat_to_B n) (nat_to_B_Nat n) ln2). rewrite - (nds_k_of_v n) - nat_to_B_diff - ndsC_v. set u := (n - Nds.nds_k_of n). have fN: natp (f (nat_to_B u)) by apply: (hc _ (nat_to_B_Nat u)). by rewrite -{1} (B_to_nat_pa fN) - nat_to_B_prod B_to_nat_pb. move: (Nds.nds_value_prop g0 g1 gn) => gp. move => n nN. rewrite - (B_to_nat_pa nN) - nds_sol_v hd. by case: (B_to_nat n); [ rewrite Nds.nds_sol0 g0 | move => m; rewrite gp]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)