proposition: Lemma nds_sol_aux k n: k <= 7 -> 0 < n < 20 -> ndsC k * nds_sol n <= nds_sol (n + k).
proof: Proof. have M m n1 n2 : (n1 <= n2) -> (n1 * m <= n2 * m). by move => h; rewrite leq_mul2r h orbT. have Hq q: 0 < q -> ndsC 1 * ndsC q <= ndsC q.+1. move => qp; apply: ltnW. rewrite !ndsCE -[ndsCb 1] /(2) /ndsCb mul2n doubleS ltnS -mul2n mulnCA - expnS. rewrite /= (prednK qp) mulSn - add1n -addSnnS leq_add2r. by rewrite -{1} [2]/(2^1) leq_exp2l. move => ha /andP [np hb]; move: ha hb. move => k7. have Hp: n < 2 -> ndsC k * nds_sol n <= nds_sol (n + k). move => n2. have : n == 1 by rewrite eqn_leq - ltnS n2 np. by move => /eqP ->; rewrite add1n nds_sol1 muln1 /nds_sol /nds_value k7. move => n20. have cv1: bin_of_nat (ndsC 1) = 2%num by rewrite ndsCE. have cv2: bin_of_nat (ndsC 2) = 5%num by rewrite ndsCE. have cv3: bin_of_nat (ndsC 3) = 13%num by rewrite ndsCE. have cv4: bin_of_nat (ndsC 4) = 33%num by rewrite ndsCE. have cv5: bin_of_nat (ndsC 5) = 81%num by rewrite ndsCE. have cv6: bin_of_nat (ndsC 6) = 193%num by rewrite ndsCE. have cv7: bin_of_nat (ndsC 7) = 449%num by rewrite ndsCE. have H a b: (bin_of_nat a < bin_of_nat b)%num -> a <= b by move/NoB_ltr /ltnW. have c6666_45555 : ndsC 6 * ndsC 6 * ndsC 6 * ndsC 6 <= ndsC 4 * ndsC 5 * ndsC 5 * ndsC 5 * ndsC 5. by apply: H; rewrite - 7! NoB_mul cv4 cv5 cv6. have c4455_666 : ndsC 4 * ndsC 4 * ndsC 5 * ndsC 5 <= ndsC 6 * ndsC 6 * ndsC 6. by apply: H; rewrite - 5! NoB_mul cv4 cv5 cv6. have c444_66 : ndsC 4 * ndsC 4 * ndsC 4 <= ndsC 6 * ndsC 6. by apply: H; rewrite - 3! NoB_mul cv4 cv6. have c77_455 : ndsC 7 * ndsC 7 <= ndsC 4 * ndsC 5 * ndsC 5. by apply: H; rewrite - 3! NoB_mul cv7 cv4 cv5. have c67_445 : ndsC 6 * ndsC 7 <= ndsC 4 * ndsC 4 * ndsC 5. by apply: H; rewrite - 3! NoB_mul cv6 cv7 cv4 cv5. have c57_66 : ndsC 5 * ndsC 7 <= ndsC 6 * ndsC 6. by apply: H; rewrite - 2! NoB_mul cv6 cv7 cv5. have c47_56 : ndsC 4 * ndsC 7 <= ndsC 5 * ndsC 6. by apply: H; rewrite - 2! NoB_mul cv6 cv7 cv5 cv4. have c37_55 : ndsC 3 * ndsC 7 <= ndsC 5 * ndsC 5. by apply: H; rewrite - 2! NoB_mul cv3 cv7 cv5. have c27_45 : ndsC 2 * ndsC 7 <= ndsC 4 * ndsC 5. by apply: H; rewrite - 2! NoB_mul cv2 cv7 cv5 cv4. have c26_35 : ndsC 2 * ndsC 6 <= ndsC 3 * ndsC 5. by apply: H; rewrite - 2! NoB_mul cv6 cv2 cv3 cv5. have c25_34 : ndsC 2 * ndsC 5 <= ndsC 3 * ndsC 4. by apply: H; rewrite - 2! NoB_mul cv2 cv3 cv4 cv5. have c24_33 : ndsC 2 * ndsC 4 <= ndsC 3 * ndsC 3. by apply: H; rewrite - 2! NoB_mul cv2 cv3 cv4. have c36_45 : ndsC 3 * ndsC 6 <= ndsC 4 * ndsC 5. by apply: H; rewrite - 2! NoB_mul cv3 cv4 cv5 cv6. have c35_44 : ndsC 3 * ndsC 5 <= ndsC 4 * ndsC 4. by apply: H; rewrite - 2! NoB_mul cv3 cv4 cv5. have c46_55 : ndsC 4 * ndsC 6 <= ndsC 5 * ndsC 5. by apply: H; rewrite - 2! NoB_mul cv6 cv4 cv5. have c23_6 : ndsC 2 * ndsC 3 <= ndsC 5. by apply: H; rewrite - NoB_mul cv2 cv3 cv5. have c22_4 : ndsC 2 * ndsC 2 <= ndsC 4. by apply: H; rewrite - ! NoB_mul cv2 cv4. have c34_7 : ndsC 3 * ndsC 4 <= ndsC 7. by apply: H; rewrite - NoB_mul cv4 cv3 cv7. have c33_6 : ndsC 3 * ndsC 3 <= ndsC 6. by apply: H; rewrite - ! NoB_mul cv3 cv6. have c24_6 := (leq_trans c24_33 c33_6). have c255_62: ndsC 2 * ndsC 5 * ndsC 5 <= ndsC 6 ^ 2. apply: (leq_trans (M (ndsC 5) _ _ c25_34)). by rewrite mulnAC - mulnn; apply: (leq_trans (M (ndsC 4) _ _ c35_44)). have c26_44:= (leq_trans c26_35 c35_44). have c17_44: ndsC 1 * ndsC 7 <= ndsC 4 ^ 2 by apply: H; rewrite - mulnn - 2! NoB_mul cv1 cv4 cv7. have c25_7:= (leq_trans c25_34 c34_7). have c366_555: (ndsC 3 * ndsC 6 * ndsC 6 <= (ndsC 5) ^3). apply: (leq_trans(M (ndsC 6) _ _ c36_45)). by rewrite mulnAC expnSr - mulnn; apply: M. have c344_56: ndsC 3 * ndsC 4 * ndsC 4 <= ndsC 5 * ndsC 6. by apply: (leq_trans(M (ndsC 4) _ _ c34_7)); rewrite mulnC. have c345_66: ndsC 3 * ndsC 4 * ndsC 5 <= ndsC 6 * ndsC 6. by apply: (leq_trans(M (ndsC 5) _ _ c34_7)); rewrite mulnC. have c_456_555: ndsC 4 * ndsC 5 * ndsC 6 <= ndsC 5 ^ 3. by rewrite mulnAC expnS - mulnn mulnA; apply:M. have E4: (ndsC 4) ^5 <= (ndsC 5) ^4. rewrite 3! expnS 2!mulnA; apply: (leq_trans (M ((ndsC 4) ^2) _ _ c444_66)). by rewrite - mulnn mulnACA mulnC mulnn -{4}[4]/(2 * 2) expnM leq_sqr - mulnn. have E5: (ndsC 6) ^5 <= (ndsC 5) ^6. rewrite 3!expnSr - mulnn; apply: (leq_trans (M (ndsC 6) _ _ c6666_45555)). rewrite - (mulnA (ndsC 4)) mulnn - (mulnA (ndsC 4)) - expnSr. rewrite - (mulnA (ndsC 4)) - expnSr mulnAC (expnS _ 5) (expnS _ 4) mulnA. by apply: M. move: k7 n20. rewrite leq_eqVlt; case/orP => k7. rewrite (eqnP k7) ltnS leq_eqVlt; case/orP => n19. rewrite (eqnP n19) nds_sol19 nds_sol26. rewrite mulnC expnSr - mulnA mulnC. apply: (leq_trans (M (ndsC 6 ^2) _ _ c67_445)). rewrite mulnn mulnAC -expnMn (expnSr _ 4); apply: M. by rewrite -{4}[4]/(2 * 2) expnM leq_sqr - mulnn. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. rewrite (eqnP n18) nds_sol18 nds_sol25 mulnA mulnAC - mulnn mulnA. rewrite expnSr mulnA (mulnC (ndsC 7)); apply: (M). apply:(leq_trans (M (ndsC 6) _ _ c67_445)). rewrite expnS mulnA (mulnC _ (_ ^2)) - mulnn (mulnAC (ndsC 4)) - mulnA. by rewrite mulnC; apply M. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. rewrite (eqP n17) nds_sol17 nds_sol24 - mulnn - mulnA mulnCA mulnA. by rewrite expnS (mulnA (ndsC 5)) (mulnC _ (_ ^2)); apply: M. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. rewrite (eqP n16) nds_sol16 nds_sol23 expnS mulnA (mulnC (ndsC 7)). by rewrite (mulnC (_ ^2)) - (mulnn (ndsC 6)); apply: M. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. rewrite (eqP n15) nds_sol15 nds_sol22 mulnA (expnSr _ 2). by rewrite (mulnC (ndsC 7)) -(mulnA (_ ^2))(mulnC ((ndsC 5)^2)); apply: M. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol21 mulnA (expnSr _ 3); apply: (M). rewrite -mulnn mulnA (mulnC (ndsC 7)). by apply: (leq_trans (M (ndsC 4) _ _ c47_56)); rewrite mulnC mulnA. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. rewrite (eqP n13) nds_sol13 nds_sol20 - mulnn mulnCA mulnA. apply: (leq_trans (M (ndsC 6) _ _ c67_445)). rewrite -mulnA mulnACA (mulnC _ (ndsC 6)) (mulnC _ (_ ^3)) mulnA. by apply:M. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. rewrite (eqP n12) nds_sol12 nds_sol19 expnS - mulnn 2! mulnA. by rewrite (mulnC (ndsC 7)); apply:M. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. rewrite (eqP n11) nds_sol11 nds_sol18 -2! mulnn. by rewrite mulnCA mulnA (mulnC _ (_ * _)); apply:M. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. rewrite (eqP n10) nds_sol10 nds_sol17 mulnCA mulnA. by rewrite - mulnn (mulnAC _ _ (ndsC 6)); apply:M. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. rewrite (eqP n9) nds_sol9 nds_sol16 - mulnn mulnCA mulnA. by apply: (leq_trans (M (ndsC 4) _ _ c47_56)); rewrite mulnC mulnA. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol15 - mulnn mulnA. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol14 mulnC - mulnn. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol13 mulnC - mulnn. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol12 mulnC. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol11 mulnC - mulnn. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol10 mulnC. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol9 mulnC. rewrite - (eqP k7); apply: (Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7. rewrite (eqP k7) ltnS leq_eqVlt; case/orP => n19. rewrite (eqP n19) nds_sol19 nds_sol25. by rewrite expnS - mulnn 2!expnS - mulnn !mulnA. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. by rewrite (eqP n18) nds_sol18 nds_sol24 mulnCA - expnS. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. by rewrite (eqP n17) nds_sol17 nds_sol23 mulnC - mulnA mulnn. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. by rewrite (eqP n16) nds_sol16 nds_sol22 mulnC. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. rewrite (eqP n15) nds_sol15 nds_sol21 mulnA (mulnC (ndsC 6)). by rewrite (expnS _ 3) (expnS _ 2) mulnA; apply: M. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol20 - mulnn expnSr !mulnA. apply:(M); rewrite (mulnC (ndsC 6)) (mulnC (ndsC 4) (ndsC 5)). by rewrite (mulnAC (ndsC 5)); apply:M. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. by rewrite (eqP n13) nds_sol13 nds_sol19. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. by rewrite (eqP n12) nds_sol12 nds_sol18 mulnCA mulnn. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. by rewrite (eqP n11) nds_sol11 nds_sol17 mulnC. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. by rewrite (eqP n10) nds_sol10 nds_sol16 mulnC. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. rewrite (eqP n9) nds_sol9 nds_sol15 -2! mulnn mulnA (mulnC (ndsC 4)). by apply:M; rewrite mulnC. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol14 -mulnn. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol13 mulnn. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol12 mulnC. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol11 mulnC - mulnn. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol10 mulnC. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol9 mulnC - mulnn. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol8 mulnC; apply: Hq. by rewrite -(eqP k7);apply: (Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7. rewrite (eqP k7) ltnS leq_eqVlt; case/orP => n19. by rewrite (eqP n19) nds_sol19 nds_sol24. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. by rewrite (eqP n18) nds_sol18 nds_sol23 mulnA mulnn. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. by rewrite (eqP n17) nds_sol17 nds_sol22 mulnA - expnS. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. by rewrite (eqP n16) nds_sol16 nds_sol21 - expnS. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. by rewrite (eqP n15) nds_sol15 nds_sol20 mulnCA - expnS. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. by rewrite (eqP n14) nds_sol14 nds_sol19 mulnC - mulnn expnS - mulnn mulnA. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. by rewrite (eqP n13) nds_sol13 nds_sol18. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. by rewrite (eqP n12) nds_sol12 nds_sol17 mulnA -mulnn. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. by rewrite (eqP n11) nds_sol11 nds_sol16 - expnS. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. by rewrite (eqP n10) nds_sol10 nds_sol15 mulnC - mulnA mulnn. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. by rewrite (eqP n9) nds_sol9 nds_sol14 mulnC. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol13. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol12. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol11. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol10 mulnC. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol9 mulnC -mulnn. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol8 mulnC. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol7 mulnC; apply: Hq. by rewrite - (eqP k7); apply: (Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7. rewrite (eqP k7) ltnS leq_eqVlt; case/orP => n19. rewrite (eqP n19) nds_sol19 nds_sol23. by rewrite expnS mulnA -(mulnn (ndsC 5)); apply: M. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. rewrite (eqP n18) nds_sol18 nds_sol22 - mulnn (mulnCA (ndsC 5)) mulnA. by rewrite expnSr - (mulnA (_ ^2)) - mulnn; apply: M. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. rewrite (eqP n17) nds_sol17 nds_sol21 mulnA mulnAC (expnS _ 3) (expnS _ 2). by rewrite mulnA; apply:M. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. by rewrite (eqP n16) nds_sol16 nds_sol20. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. by rewrite (eqP n15) nds_sol15 nds_sol19 - mulnn expnS - mulnn !mulnA. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol18 - 2!mulnn mulnA. by rewrite (mulnC (ndsC 5)) mulnA; apply: M. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. by rewrite (eqP n13) nds_sol13 nds_sol17 -2!mulnn mulnA; apply: M. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. by rewrite (eqP n12) nds_sol12 nds_sol16 mulnA. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. by rewrite (eqP n11) nds_sol11 nds_sol15. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. by rewrite (eqP n10) nds_sol10 nds_sol14 mulnA mulnn. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. by rewrite (eqP n9) nds_sol9 nds_sol13 -2! mulnn mulnA. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol12. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol11 - mulnn. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol10. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol9 mulnn. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol8 mulnC. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol7 mulnC. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol6 mulnC; apply: Hq. by rewrite - (eqP k7); apply:(Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7. rewrite (eqP k7) ltnS leq_eqVlt; case/orP => n19. rewrite (eqP n19) nds_sol19 nds_sol22. by rewrite expnSr mulnA; apply: M; rewrite - mulnn mulnA. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. rewrite (eqP n18) nds_sol18 nds_sol21 mulnA mulnAC - mulnn mulnA expnSr. by apply: M. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. rewrite (eqP n17) nds_sol17 nds_sol20 mulnA mulnAC (expnS _ 2) mulnA. by apply: M. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. rewrite (eqP n16) nds_sol16 nds_sol19 expnS mulnA. apply: (leq_trans(M ((ndsC 5) ^2) _ _ c35_44)). by rewrite -mulnn expnS - mulnn ! mulnA. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. rewrite (eqP n15) nds_sol15 nds_sol18 (mulnC (ndsC 5)) - 2! mulnn. by rewrite !mulnA; apply: M. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol17 mulnA - mulnn. by rewrite -mulnn (mulnAC (ndsC 5)) mulnA; apply: M. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. rewrite (eqP n13) nds_sol13 nds_sol16 - mulnn mulnA. apply: (leq_trans(M (ndsC 6) _ _ c36_45)). by rewrite mulnAC expnSr - mulnn; apply:M. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. rewrite (eqP n12) nds_sol12 nds_sol15 mulnA mulnAC - mulnn mulnA. by apply: (leq_trans(M (ndsC 5) _ _ c36_45)). move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. rewrite (eqP n11) nds_sol11 nds_sol14 - mulnn - mulnn ! mulnA. by apply: (leq_trans(M (ndsC 5) _ _ c35_44)). move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. by rewrite (eqP n10) nds_sol10 nds_sol13 mulnA - mulnn. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. by rewrite (eqP n9) nds_sol9 nds_sol12 - mulnn mulnA. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol11 - mulnn. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol10. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol9 - mulnn. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol8. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol7. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol6 mulnC. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol5 mulnC; apply: Hq. rewrite -(eqP k7); apply: (Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7. rewrite (eqP k7). rewrite ltnS leq_eqVlt; case/orP => n19. rewrite (eqP n19) nds_sol19 nds_sol21 expnS mulnA. apply: (leq_trans (M (ndsC 6 ^ 2) _ _ c26_35)). rewrite mulnAC (expnSr _ 3); apply: (M). rewrite - mulnn mulnA;apply:(leq_trans (M (ndsC 6) _ _ c36_45)). by rewrite mulnAC expnS - mulnn mulnA; apply:M. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. rewrite (eqP n18) nds_sol18 nds_sol20 mulnCA mulnC - mulnn. rewrite expnSr mulnA mulnA; apply: (M). apply: (leq_trans (M (ndsC 6) _ _ c26_35)). rewrite mulnAC -mulnn mulnA; apply: (M (ndsC 5) _ _ (c36_45)). move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. rewrite (eqP n17) nds_sol17 nds_sol19 mulnA - mulnn expnSr mulnA. by apply:M. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. rewrite (eqP n16) nds_sol16 nds_sol18 expnSr mulnA (mulnC (ndsC 5)). by apply: M; rewrite - mulnn mulnA -mulnn. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. rewrite (eqP n15) nds_sol15 nds_sol17 mulnA (mulnC _ (ndsC 6)). by apply: M. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol16 mulnA - mulnn expnSr - mulnn mulnA. apply: (M); apply (leq_trans (M (ndsC 4) _ _ c24_6)). by rewrite mulnC. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. rewrite (eqP n13) nds_sol13 nds_sol15 - !mulnn mulnA mulnA. apply (leq_trans (M (ndsC 6) _ _ c26_35)). by rewrite mulnAC; apply: M. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. rewrite (eqP n12) nds_sol12 nds_sol14 - mulnn mulnA mulnAC. by apply: M. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. by rewrite (eqP n11) nds_sol11 nds_sol13 -mulnn mulnA. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. rewrite (eqP n10) nds_sol10 nds_sol12 mulnA (mulnC _ (ndsC 6)). by apply: M. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. rewrite (eqP n9) nds_sol9 nds_sol11 - mulnn - mulnn mulnA. by apply: (leq_trans (M (ndsC 4) _ _ c24_6)); rewrite mulnC. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol10. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol9 - mulnn. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol8. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol7. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol6. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol5. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol4 mulnC; apply: Hq. rewrite -(eqP k7); apply: (Hp n2). move: k7; rewrite ltnS leq_eqVlt; case/orP => k7; last first. move => _; move: k7; rewrite ltnS leqn0 => /eqP ->. rewrite ndsC0 mul1n addn0. rewrite leqnn; exact: isT. rewrite (eqP k7) ltnS leq_eqVlt; case/orP => n19. rewrite (eqP n19) nds_sol19 nds_sol20 expnS mulnA. apply: (leq_trans (M (ndsC 6 ^ 2) _ _ (Hq 6 isT))). rewrite - mulnn mulnA (mulnC (ndsC 7)). apply: (leq_trans (M (ndsC 6) _ _ (c67_445))). rewrite expnSr mulnA mulnAC; apply: (M). by rewrite - mulnA mulnC (mulnC _ (_ ^ 2)) - mulnn; apply: M. move: n19; rewrite ltnS leq_eqVlt; case/orP => n18. rewrite (eqP n18) nds_sol18 nds_sol19 mulnA (expnS _ 2). by apply: M; apply: Hq. move: n18; rewrite ltnS leq_eqVlt; case/orP => n17. rewrite (eqP n17) nds_sol17 nds_sol18 - mulnn - mulnn (mulnCA (ndsC 5)). by rewrite mulnA mulnA - (mulnA _ _ (ndsC 6)); apply: M; apply: Hq. move: n17; rewrite ltnS leq_eqVlt; case/orP => n16. rewrite (eqP n16) nds_sol16 nds_sol17 expnS mulnA (mulnC _ (ndsC 6)). by apply: M; apply: Hq. move: n16; rewrite ltnS leq_eqVlt; case/orP => n15. rewrite (eqP n15) nds_sol15 nds_sol16 (expnS _ 2) mulnA. by apply: M; apply: Hq. move: n15; rewrite ltnS leq_eqVlt; case/orP => n14. rewrite (eqP n14) nds_sol14 nds_sol15 - mulnn - mulnn. rewrite mulnA mulnA mulnCA - (mulnA _ _ (ndsC 5)). by apply: M; apply: Hq. move: n14; rewrite ltnS leq_eqVlt; case/orP => n13. rewrite (eqP n13) nds_sol13 nds_sol14 - mulnn - mulnn mulnA. by apply: (leq_trans (M (ndsC 6) _ _ (Hq 6 isT))); rewrite mulnC. move: n13; rewrite ltnS leq_eqVlt; case/orP => n12. rewrite (eqP n12) nds_sol12 nds_sol13 mulnA - mulnn. by apply: M; apply: Hq. move: n12; rewrite ltnS leq_eqVlt; case/orP => n11. rewrite (eqP n11) nds_sol11 nds_sol12 - mulnn mulnA (mulnC (ndsC 5)). by apply: M; apply: Hq. move: n11; rewrite ltnS leq_eqVlt; case/orP => n10. rewrite (eqP n10) nds_sol10 nds_sol11 - mulnn mulnA. by apply: M; apply: Hq. move: n10; rewrite ltnS leq_eqVlt; case/orP => n9. rewrite (eqP n9) nds_sol9 nds_sol10 - mulnn mulnA (mulnC (ndsC 4)). by apply: M; apply: Hq. move: n9; rewrite ltnS leq_eqVlt; case/orP => n8. by rewrite (eqP n8) nds_sol8 nds_sol9; apply: c17_44. move: n8; rewrite ltnS leq_eqVlt; case/orP => n7. by rewrite (eqP n7) nds_sol7 nds_sol8; apply: Hq. move: n7; rewrite ltnS leq_eqVlt; case/orP => n6. by rewrite (eqP n6) nds_sol6 nds_sol7; apply: Hq. move: n6; rewrite ltnS leq_eqVlt; case/orP => n5. by rewrite (eqP n5) nds_sol5 nds_sol6; apply: Hq. move: n5; rewrite ltnS leq_eqVlt; case/orP => n4. by rewrite (eqP n4) nds_sol4 nds_sol5; apply: Hq. move: n4; rewrite ltnS leq_eqVlt; case/orP => n3. by rewrite (eqP n3) nds_sol3 nds_sol4; apply: Hq. move: n3; rewrite ltnS leq_eqVlt; case/orP => n2. by rewrite (eqP n2) nds_sol2 nds_sol3; apply: Hq. rewrite -(eqP k7); apply: (Hp n2). Qed.
imports: Coq(BinNat) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div)