proposition: Lemma nds_sol_with_k n: 1 < n -> nds_sol n = (ndsC (nds_k_of n)) * nds_sol (n - (nds_k_of n)).
proof: Proof. move => l1n. move: (ltn_predK l1n) => np. have -> : (n - (nds_k_of n)) = (n.-1 - (nds_k_of n)).+1. move:(nds_k_of_bd l1n) =>/andP[_]; rewrite - {2 3} np ltnS => eqa. by rewrite - (subSn eqa). rewrite - {1} np /nds_k_of /nds_sol /nds_value. rewrite - ltnS np. case: (ltnP 8 n); last by rewrite subnn /= ndsC0 muln1. case n9: (n == 9) => en8. have ->: (n.-1 - 4) = 4 by rewrite (eqP n9). have ->: n.-1 %% 5 = 3 by rewrite (eqP n9). have ->: n.-1 %/ 5 == 1 by rewrite (eqP n9). by rewrite /= mulnn. case n13: (n == 13). have ->: (n.-1 - 6) = 6 by rewrite (eqP n13). have ->: n.-1 %% 5 = 2 by rewrite (eqP n13). have ->: (n.-1 %/ 5).-2 = 0 by rewrite (eqP n13). by rewrite /= expn0 muln1 mulnn. case n19: (n == 19). have ->: (n.-1 - 6) = 12 by rewrite (eqP n19). have ->: n.-1 %% 5 = 3 by rewrite (eqP n19). have ->: n.-1 %/ 5 = 3 by rewrite (eqP n19). by rewrite /= subnn expn0 mulnA - expnS. set m := n.-1 - 5. have mv : n.-1 = m + 5. rewrite /m subnK // - ltnS np; exact (leq_trans (isT: 6 <= 9) en8). have l4m: 4 <= m. by rewrite - (leq_add2r 5) - mv - ltnS np ltn_neqAle en8 andbT eq_sym n9. rewrite mv modnDr. case: (ltnP 7 m); last first. rewrite leq_eqVlt ltnS leq_eqVlt ltnS leq_eqVlt; case/or4P. + move => lt1. suff w: (n == 13) by move: n13; rewrite w. by rewrite - np mv (eqP lt1). + by move/eqP ->; rewrite /= expn1 mulnC. + by move/eqP ->; rewrite /= mulnn. + move => lt1. have: m == 4 by rewrite eqn_leq - ltnS lt1 l4m. by move/eqP ->; rewrite /= expn1 mulnC. move: (@divnMDl 1 m 5 isT); rewrite mul1n addnC add1n => ->. move => lm7. move: (divn_eq m 5) => qr. move: (ltn_pmod m (isT: 0 < 5)) => lr5. have qp: (0 < m %/ 5). move: (leq_trans (isT: 5 <= 8) lm7). by rewrite {1} qr; case (m %/ 5) => //; rewrite add0n leqNgt lr5. case: ifP; first by rewrite - expnS. case: ifP; first by rewrite mulnCA - expnS (prednK qp). case: ifP. move => r2; rewrite /= mulnCA - expnS. have hu: 2 <= (m %/ 5). rewrite ltn_neqAle qp andbT. apply/negP => /eqP q1; suff w: (n == 13) by move: n13; rewrite w. by rewrite - np mv qr - q1 (eqP r2). by rewrite - {1} (subnK hu) subn2 addn2. case: ifP; last by rewrite mulnCA - expnS. rewrite eqSS eqSS; move: (ltn_eqF qp); rewrite eq_sym => ->. case q5: (m %/ 5 == 1); first by rewrite mulnC. case q7: (m %/ 5 == 2) => r3 _ _ _. suff w: (n == 19) by move: n19; rewrite w. by rewrite - np mv qr (eqP r3) (eqP q7). rewrite mulnCA - expnS; congr (_ * _ ^ _). move: qp q5 q7; case: ((m %/ 5)) => //; case => //; case => // q _ _ _. by rewrite - addn3 addnK - addn3 addnK. Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)