proposition: Lemma nds_sol_bd n k: 2 <= n -> 0 < k < n -> (ndsC k) * (nds_sol (n - k)) <= nds_sol n.
proof: Proof. move => ha /andP [kp lkn]. rewrite -{2} (subnK (ltnW lkn)). have: 0 < n - k by rewrite subn_gt0. move:(n-k). clear n ha kp lkn. pose P k := forall n, 0 <n -> ndsC k * nds_sol n <= nds_sol (n + k). rewrite -/(P k); move: k. have Hb q: 4 <= q -> ndsC (q .*2.+1) < ndsC q * ndsC q.+1. move => le4q. have qp: 0 < q by move: le4q; case q. rewrite !ndsCE /ndsCb. set t := 2 ^ q.-1. have tp: 0 < t by rewrite expn_gt0. have tp': 0 < 2 ^q by rewrite expn_gt0. have ->: 2 ^ q.*2 = 2^(q.+1) * t. by rewrite - addnn -{2} (prednK qp) - addSnnS expnD. have le1: q.*2.+1 * 2 * 2 ^ q <= q * q.+1 * 2 ^ q. rewrite (leq_pmul2r tp') mulSn (mulnS q). apply: (leq_add (ltnW (ltnW le4q))). rewrite - muln2 - mulnA. by rewrite (leq_pmul2l). rewrite (mulSnr (q*t)) mulnSr addnS ltnS - {2}[in 2^q] (prednK qp). rewrite !expnS (mulnAC q t) - mulnDl ! mulnA - mulnDl (ltn_pmul2r tp). apply:(leq_ltn_trans le1). by rewrite -addn1 - addnA leq_add2l -{1} (prednK qp) addSn ltnS. have Ha q: 4 <= q -> ndsC (q .*2) < ndsC q * ndsC q. move => le4q. have qp: 0 < q by move: le4q; case (q). rewrite !ndsCE /ndsCb. set t := 2 ^ q.-1. have qtp: 0 < q * t by rewrite muln_gt0 qp expn_gt0. have -> : 2 ^ q.*2.-1 = (t *t).*2. by rewrite - (prednK qp) doubleS expnS - addnn expnD mul2n. have ->: q.*2 * (t * t).*2 = (q * t) * (t * 4). by rewrite - !muln2 - mulnA (mulnC 2) -[4]/(2 *2) !mulnA. rewrite (mulnSr (q * t).+1) addnS ltnS - mulSnr mulnC. by rewrite (ltn_pmul2r qtp) ltnS ltnW // ltnS mulnC leq_mul. have h: (forall k, k <=7 -> P k). move => k lk7 n. elim: n {1 3 4 5} n (leqnn n). by move => n; rewrite leqn0 => /eqP ->. move => n Hr m; rewrite leq_eqVlt ltnS; case/orP; last by apply: Hr. move /eqP ->. case: (ltnP n.+1 20) => n20; first by move => _; apply: nds_sol_aux. have n5: 5 <= n.+1 by apply: leq_trans n20. have sn5: 0 < n.+1 - 5. by rewrite -(leq_add2r 5) (subnK n5); apply: leq_trans n20. move: (subnK n5) => dv _. have dkv: n.+1 + k - 5 + 5 = n.+1 + k. by rewrite (addnC n.+1 k) - (addnBA _ n5) - addnA dv. have n15: 14 < n.+1 - 5 by rewrite - (leq_add2r 5) dv. have nk15: 14 < (n.+1 + k) - 5. rewrite - (leq_add2r 5) dkv; apply: (leq_trans n20); apply: leq_addr. have ltrec: n.+1 - 5 <= n by rewrite - (leq_add2r 5) dv -addn1 leq_add2l. rewrite - dkv (nds_sol_rec5 nk15) -{1} dv (nds_sol_rec5 n15) mulnCA leq_mul2l. by rewrite (addnC n.+1 k) -(addnBA _ n5) addnC (Hr _ ltrec sn5) orbT. move => k; elim: k {1 3} (k) (leqnn k). by move => k; rewrite leqn0 => /eqP ->; apply: h. move => n Hr k; rewrite leq_eqVlt ltnS; case /orP; last by apply: Hr. move /eqP ->. case: (ltnP n 7); [by apply: h | rewrite -ltnS; move => n7]. have lnn: n < n.*2. by rewrite - addn1 - addnn leq_add2l - ltnS; apply: leq_trans n7. move:(odd_double_half (n.+1)); case: odd. set q := (n.+1)./2; rewrite add1n => qv. have /Hb : 3 < q by rewrite - leq_Sdouble qv. rewrite qv => /ltnW lt1. move => m mp. have aux: 0 < m + q.+1 by rewrite addnS ltnS. apply: (@leq_trans (ndsC q * (ndsC q.+1 * (nds_sol m)))). by rewrite mulnA leq_mul2r lt1 orbT. have la: q.+1 <= n by rewrite - ltn_double qv. move: (Hr q (ltnW la) (m + q.+1) aux); rewrite -addnA addSn addnn qv. by apply: leq_trans; rewrite leq_mul2l (Hr q.+1 la _ mp) orbT. set q := (n.+1)./2; rewrite add0n => qv. have /Ha : 3 < q by rewrite - leq_double qv. rewrite qv => /ltnW lt1 m mp. have aux: 0 < m + q by apply: (leq_trans mp); apply: leq_addr. apply: (@leq_trans (ndsC q * (ndsC q * (nds_sol m)))). by rewrite mulnA leq_mul2r lt1 orbT. have la: q <= n by rewrite - leq_double - ltnS qv ltnS. move: (Hr q la _ aux); rewrite -addnA addnn qv. by apply: leq_trans; rewrite leq_mul2l (Hr q la m mp) orbT. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)