proposition: Lemma nds_alt f: f \0c = \1c -> f \1c = \1c -> (forall n, natp n -> \1c <c n -> exists k, [/\ \0c <c k, k <c n & f n <=c (ndsC k) *c f (n -c k)]) -> (forall n, natp n -> nds_sol (csucc n) <=c f (csucc n)) -> (forall n, natp n -> f n = nds_sol n).
proof: Proof. move => f0 f1 hf1 hf2. 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:(hf1 _ snN sn1) => [k [ka kb kc]]. move:(cdiff_ltb snN (proj1 kb) (nesym (proj2 ka))) => /(cltSleP nN) le1. apply: (NS_le_nat kc); apply: (NS_prod (NS_ndsC (NS_lt_nat kb snN))). by apply: Hr. 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 gp2: forall n, Nds.nds_sol n.+1 <= g n.+1. move => n; apply/nat_to_B_le; rewrite - hd nds_sol_v /=; apply: hf2. by apply: nat_to_B_Nat. have gp1:forall n, 1 < n -> exists2 k, 0 < k < n & g n <= Nds.ndsC k * g (n - k). move => n /nat_to_B_lt; rewrite nat_to_B1 => np. have nN := (nat_to_B_Nat n). move: (hf1 _ nN np) => [k [ka kb kc]]. move: (B_to_nat_pa (NS_lt_nat kb nN)) => kv. exists (B_to_nat k). apply/andP; split; [ apply/nat_to_B_pos; ue | apply/nat_to_B_lt; ue]. apply/nat_to_B_le; rewrite /g nat_to_B_diff kv (B_to_nat_pa (hc _ nN)). by rewrite nat_to_B_prod ndsC_v kv (B_to_nat_pa (hc _ (NS_diff _ nN))). move: (Nds.nds_alt g0 g1 gp1 gp2) => OK. move => n /B_to_nat_pa <-. case: (B_to_nat n); first by rewrite /= f0 /nds_sol; Ytac0. by move => k; rewrite - nds_sol_v OK //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)