pow_six_ten_le_pow_four_thirteen_from_total

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

1. 0001intro x
2. 0002intro y
3. 0003intro htotal
4. 0004intro hx
5. 0005intro hy
6. 0006have hthree_five : exists q. (exists pa_b_hj32_row4_three_five pa_c_hj32_row4_three_five. ((forall pa_i_hj32_row4_three_five_repeat. (exists pa_lt_hj32_row4_three_five_repeat_bound. pa_lt_hj32_row4_three_five_repeat_bound + S pa_i_hj32_row4_three_five_repeat = 5) -> (((exists pa_h_hj32_row4_three_five_repeat_decoded. pa_h_hj32_row4_three_five_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_five_repeat)) * pa_c_hj32_row4_three_five)) /\ exists pa_q_hj32_row4_three_five_repeat_decoded. pa_b_hj32_row4_three_five = pa_q_hj32_row4_three_five_repeat_decoded * S ((S (pa_i_hj32_row4_three_five_repeat)) * pa_c_hj32_row4_three_five) + (3)))) /\ (exists pa_u_hj32_row4_three_five_product pa_v_hj32_row4_three_five_product. ((((exists pa_h_hj32_row4_three_five_product_start. pa_h_hj32_row4_three_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_start. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_start * S ((S (0)) * pa_v_hj32_row4_three_five_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_five_product_terminal. pa_h_hj32_row4_three_five_product_terminal + S (q) = S ((S (5)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_terminal. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_terminal * S ((S (5)) * pa_v_hj32_row4_three_five_product) + (q))) /\ forall pa_i_hj32_row4_three_five_product. (exists pa_lt_hj32_row4_three_five_product_bound. pa_lt_hj32_row4_three_five_product_bound + S pa_i_hj32_row4_three_five_product = 5) -> exists pa_p_hj32_row4_three_five_product pa_r_hj32_row4_three_five_product pa_s_hj32_row4_three_five_product. ((((exists pa_h_hj32_row4_three_five_product_factor. pa_h_hj32_row4_three_five_product_factor + S (pa_p_hj32_row4_three_five_product) = S ((S (pa_i_hj32_row4_three_five_product)) * pa_c_hj32_row4_three_five)) /\ exists pa_q_hj32_row4_three_five_product_factor. pa_b_hj32_row4_three_five = pa_q_hj32_row4_three_five_product_factor * S ((S (pa_i_hj32_row4_three_five_product)) * pa_c_hj32_row4_three_five) + (pa_p_hj32_row4_three_five_product))) /\ ((((exists pa_h_hj32_row4_three_five_product_partial. pa_h_hj32_row4_three_five_product_partial + S (pa_r_hj32_row4_three_five_product) = S ((S (pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_partial. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_partial * S ((S (pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product) + (pa_r_hj32_row4_three_five_product))) /\ ((((exists pa_h_hj32_row4_three_five_product_successor. pa_h_hj32_row4_three_five_product_successor + S (pa_s_hj32_row4_three_five_product) = S ((S (S pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product)) /\ exists pa_q_hj32_row4_three_five_product_successor. pa_u_hj32_row4_three_five_product = pa_q_hj32_row4_three_five_product_successor * S ((S (S pa_i_hj32_row4_three_five_product)) * pa_v_hj32_row4_three_five_product) + (pa_s_hj32_row4_three_five_product))) /\ pa_s_hj32_row4_three_five_product = pa_r_hj32_row4_three_five_product * pa_p_hj32_row4_three_five_product))))))))
7. 0007specialize htotal 3
8. 0008specialize htotal 5
9. 0009exact htotal
10. 0010cases hthree_five
11. 0011have hfour_four : exists q. (exists pa_b_hj32_row4_four_four pa_c_hj32_row4_four_four. ((forall pa_i_hj32_row4_four_four_repeat. (exists pa_lt_hj32_row4_four_four_repeat_bound. pa_lt_hj32_row4_four_four_repeat_bound + S pa_i_hj32_row4_four_four_repeat = 4) -> (((exists pa_h_hj32_row4_four_four_repeat_decoded. pa_h_hj32_row4_four_four_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_four_repeat)) * pa_c_hj32_row4_four_four)) /\ exists pa_q_hj32_row4_four_four_repeat_decoded. pa_b_hj32_row4_four_four = pa_q_hj32_row4_four_four_repeat_decoded * S ((S (pa_i_hj32_row4_four_four_repeat)) * pa_c_hj32_row4_four_four) + (4)))) /\ (exists pa_u_hj32_row4_four_four_product pa_v_hj32_row4_four_four_product. ((((exists pa_h_hj32_row4_four_four_product_start. pa_h_hj32_row4_four_four_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_start. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_start * S ((S (0)) * pa_v_hj32_row4_four_four_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_four_product_terminal. pa_h_hj32_row4_four_four_product_terminal + S (q) = S ((S (4)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_terminal. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_terminal * S ((S (4)) * pa_v_hj32_row4_four_four_product) + (q))) /\ forall pa_i_hj32_row4_four_four_product. (exists pa_lt_hj32_row4_four_four_product_bound. pa_lt_hj32_row4_four_four_product_bound + S pa_i_hj32_row4_four_four_product = 4) -> exists pa_p_hj32_row4_four_four_product pa_r_hj32_row4_four_four_product pa_s_hj32_row4_four_four_product. ((((exists pa_h_hj32_row4_four_four_product_factor. pa_h_hj32_row4_four_four_product_factor + S (pa_p_hj32_row4_four_four_product) = S ((S (pa_i_hj32_row4_four_four_product)) * pa_c_hj32_row4_four_four)) /\ exists pa_q_hj32_row4_four_four_product_factor. pa_b_hj32_row4_four_four = pa_q_hj32_row4_four_four_product_factor * S ((S (pa_i_hj32_row4_four_four_product)) * pa_c_hj32_row4_four_four) + (pa_p_hj32_row4_four_four_product))) /\ ((((exists pa_h_hj32_row4_four_four_product_partial. pa_h_hj32_row4_four_four_product_partial + S (pa_r_hj32_row4_four_four_product) = S ((S (pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_partial. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_partial * S ((S (pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product) + (pa_r_hj32_row4_four_four_product))) /\ ((((exists pa_h_hj32_row4_four_four_product_successor. pa_h_hj32_row4_four_four_product_successor + S (pa_s_hj32_row4_four_four_product) = S ((S (S pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product)) /\ exists pa_q_hj32_row4_four_four_product_successor. pa_u_hj32_row4_four_four_product = pa_q_hj32_row4_four_four_product_successor * S ((S (S pa_i_hj32_row4_four_four_product)) * pa_v_hj32_row4_four_four_product) + (pa_s_hj32_row4_four_four_product))) /\ pa_s_hj32_row4_four_four_product = pa_r_hj32_row4_four_four_product * pa_p_hj32_row4_four_four_product))))))))
12. 0012specialize htotal 4
13. 0013specialize htotal 4
14. 0014exact htotal
15. 0015cases hfour_four
16. 0016have hseed : exists bqb_le_gap_hj32_row4_seed_bound. bqb_le_gap_hj32_row4_seed_bound + (x1) = (x2)
17. 0017specialize pow_three_five_le_pow_four_four_from_total x1
18. 0018specialize pow_three_five_le_pow_four_four_from_total x2
19. 0019apply pow_three_five_le_pow_four_four_from_total
20. 0020exact htotal
21. 0021exact hthree_five_witness
22. 0022exact hfour_four_witness
23. 0023have hthree_ten : exists q. (exists pa_b_hj32_row4_three_ten pa_c_hj32_row4_three_ten. ((forall pa_i_hj32_row4_three_ten_repeat. (exists pa_lt_hj32_row4_three_ten_repeat_bound. pa_lt_hj32_row4_three_ten_repeat_bound + S pa_i_hj32_row4_three_ten_repeat = 10) -> (((exists pa_h_hj32_row4_three_ten_repeat_decoded. pa_h_hj32_row4_three_ten_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_ten_repeat)) * pa_c_hj32_row4_three_ten)) /\ exists pa_q_hj32_row4_three_ten_repeat_decoded. pa_b_hj32_row4_three_ten = pa_q_hj32_row4_three_ten_repeat_decoded * S ((S (pa_i_hj32_row4_three_ten_repeat)) * pa_c_hj32_row4_three_ten) + (3)))) /\ (exists pa_u_hj32_row4_three_ten_product pa_v_hj32_row4_three_ten_product. ((((exists pa_h_hj32_row4_three_ten_product_start. pa_h_hj32_row4_three_ten_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_start. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_start * S ((S (0)) * pa_v_hj32_row4_three_ten_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_ten_product_terminal. pa_h_hj32_row4_three_ten_product_terminal + S (q) = S ((S (10)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_terminal. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_terminal * S ((S (10)) * pa_v_hj32_row4_three_ten_product) + (q))) /\ forall pa_i_hj32_row4_three_ten_product. (exists pa_lt_hj32_row4_three_ten_product_bound. pa_lt_hj32_row4_three_ten_product_bound + S pa_i_hj32_row4_three_ten_product = 10) -> exists pa_p_hj32_row4_three_ten_product pa_r_hj32_row4_three_ten_product pa_s_hj32_row4_three_ten_product. ((((exists pa_h_hj32_row4_three_ten_product_factor. pa_h_hj32_row4_three_ten_product_factor + S (pa_p_hj32_row4_three_ten_product) = S ((S (pa_i_hj32_row4_three_ten_product)) * pa_c_hj32_row4_three_ten)) /\ exists pa_q_hj32_row4_three_ten_product_factor. pa_b_hj32_row4_three_ten = pa_q_hj32_row4_three_ten_product_factor * S ((S (pa_i_hj32_row4_three_ten_product)) * pa_c_hj32_row4_three_ten) + (pa_p_hj32_row4_three_ten_product))) /\ ((((exists pa_h_hj32_row4_three_ten_product_partial. pa_h_hj32_row4_three_ten_product_partial + S (pa_r_hj32_row4_three_ten_product) = S ((S (pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_partial. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_partial * S ((S (pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product) + (pa_r_hj32_row4_three_ten_product))) /\ ((((exists pa_h_hj32_row4_three_ten_product_successor. pa_h_hj32_row4_three_ten_product_successor + S (pa_s_hj32_row4_three_ten_product) = S ((S (S pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product)) /\ exists pa_q_hj32_row4_three_ten_product_successor. pa_u_hj32_row4_three_ten_product = pa_q_hj32_row4_three_ten_product_successor * S ((S (S pa_i_hj32_row4_three_ten_product)) * pa_v_hj32_row4_three_ten_product) + (pa_s_hj32_row4_three_ten_product))) /\ pa_s_hj32_row4_three_ten_product = pa_r_hj32_row4_three_ten_product * pa_p_hj32_row4_three_ten_product))))))))
24. 0024specialize htotal 3
25. 0025specialize htotal 10
26. 0026exact htotal
27. 0027cases hthree_ten
28. 0028have hfour_eight : exists q. (exists pa_b_hj32_row4_four_eight pa_c_hj32_row4_four_eight. ((forall pa_i_hj32_row4_four_eight_repeat. (exists pa_lt_hj32_row4_four_eight_repeat_bound. pa_lt_hj32_row4_four_eight_repeat_bound + S pa_i_hj32_row4_four_eight_repeat = 8) -> (((exists pa_h_hj32_row4_four_eight_repeat_decoded. pa_h_hj32_row4_four_eight_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_eight_repeat)) * pa_c_hj32_row4_four_eight)) /\ exists pa_q_hj32_row4_four_eight_repeat_decoded. pa_b_hj32_row4_four_eight = pa_q_hj32_row4_four_eight_repeat_decoded * S ((S (pa_i_hj32_row4_four_eight_repeat)) * pa_c_hj32_row4_four_eight) + (4)))) /\ (exists pa_u_hj32_row4_four_eight_product pa_v_hj32_row4_four_eight_product. ((((exists pa_h_hj32_row4_four_eight_product_start. pa_h_hj32_row4_four_eight_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_start. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_start * S ((S (0)) * pa_v_hj32_row4_four_eight_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_eight_product_terminal. pa_h_hj32_row4_four_eight_product_terminal + S (q) = S ((S (8)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_terminal. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_terminal * S ((S (8)) * pa_v_hj32_row4_four_eight_product) + (q))) /\ forall pa_i_hj32_row4_four_eight_product. (exists pa_lt_hj32_row4_four_eight_product_bound. pa_lt_hj32_row4_four_eight_product_bound + S pa_i_hj32_row4_four_eight_product = 8) -> exists pa_p_hj32_row4_four_eight_product pa_r_hj32_row4_four_eight_product pa_s_hj32_row4_four_eight_product. ((((exists pa_h_hj32_row4_four_eight_product_factor. pa_h_hj32_row4_four_eight_product_factor + S (pa_p_hj32_row4_four_eight_product) = S ((S (pa_i_hj32_row4_four_eight_product)) * pa_c_hj32_row4_four_eight)) /\ exists pa_q_hj32_row4_four_eight_product_factor. pa_b_hj32_row4_four_eight = pa_q_hj32_row4_four_eight_product_factor * S ((S (pa_i_hj32_row4_four_eight_product)) * pa_c_hj32_row4_four_eight) + (pa_p_hj32_row4_four_eight_product))) /\ ((((exists pa_h_hj32_row4_four_eight_product_partial. pa_h_hj32_row4_four_eight_product_partial + S (pa_r_hj32_row4_four_eight_product) = S ((S (pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_partial. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_partial * S ((S (pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product) + (pa_r_hj32_row4_four_eight_product))) /\ ((((exists pa_h_hj32_row4_four_eight_product_successor. pa_h_hj32_row4_four_eight_product_successor + S (pa_s_hj32_row4_four_eight_product) = S ((S (S pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product)) /\ exists pa_q_hj32_row4_four_eight_product_successor. pa_u_hj32_row4_four_eight_product = pa_q_hj32_row4_four_eight_product_successor * S ((S (S pa_i_hj32_row4_four_eight_product)) * pa_v_hj32_row4_four_eight_product) + (pa_s_hj32_row4_four_eight_product))) /\ pa_s_hj32_row4_four_eight_product = pa_r_hj32_row4_four_eight_product * pa_p_hj32_row4_four_eight_product))))))))
29. 0029specialize htotal 4
30. 0030specialize htotal 8
31. 0031exact htotal
32. 0032cases hfour_eight
33. 0033have hthree_ten_block : exists pa_b_hj32_row4_three_ten_block pa_c_hj32_row4_three_ten_block. ((forall pa_i_hj32_row4_three_ten_block_repeat. (exists pa_lt_hj32_row4_three_ten_block_repeat_bound. pa_lt_hj32_row4_three_ten_block_repeat_bound + S pa_i_hj32_row4_three_ten_block_repeat = 5 * 2) -> (((exists pa_h_hj32_row4_three_ten_block_repeat_decoded. pa_h_hj32_row4_three_ten_block_repeat_decoded + S (3) = S ((S (pa_i_hj32_row4_three_ten_block_repeat)) * pa_c_hj32_row4_three_ten_block)) /\ exists pa_q_hj32_row4_three_ten_block_repeat_decoded. pa_b_hj32_row4_three_ten_block = pa_q_hj32_row4_three_ten_block_repeat_decoded * S ((S (pa_i_hj32_row4_three_ten_block_repeat)) * pa_c_hj32_row4_three_ten_block) + (3)))) /\ (exists pa_u_hj32_row4_three_ten_block_product pa_v_hj32_row4_three_ten_block_product. ((((exists pa_h_hj32_row4_three_ten_block_product_start. pa_h_hj32_row4_three_ten_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_start. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_start * S ((S (0)) * pa_v_hj32_row4_three_ten_block_product) + (1))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_terminal. pa_h_hj32_row4_three_ten_block_product_terminal + S (x3) = S ((S (5 * 2)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_terminal. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_terminal * S ((S (5 * 2)) * pa_v_hj32_row4_three_ten_block_product) + (x3))) /\ forall pa_i_hj32_row4_three_ten_block_product. (exists pa_lt_hj32_row4_three_ten_block_product_bound. pa_lt_hj32_row4_three_ten_block_product_bound + S pa_i_hj32_row4_three_ten_block_product = 5 * 2) -> exists pa_p_hj32_row4_three_ten_block_product pa_r_hj32_row4_three_ten_block_product pa_s_hj32_row4_three_ten_block_product. ((((exists pa_h_hj32_row4_three_ten_block_product_factor. pa_h_hj32_row4_three_ten_block_product_factor + S (pa_p_hj32_row4_three_ten_block_product) = S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_c_hj32_row4_three_ten_block)) /\ exists pa_q_hj32_row4_three_ten_block_product_factor. pa_b_hj32_row4_three_ten_block = pa_q_hj32_row4_three_ten_block_product_factor * S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_c_hj32_row4_three_ten_block) + (pa_p_hj32_row4_three_ten_block_product))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_partial. pa_h_hj32_row4_three_ten_block_product_partial + S (pa_r_hj32_row4_three_ten_block_product) = S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_partial. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_partial * S ((S (pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product) + (pa_r_hj32_row4_three_ten_block_product))) /\ ((((exists pa_h_hj32_row4_three_ten_block_product_successor. pa_h_hj32_row4_three_ten_block_product_successor + S (pa_s_hj32_row4_three_ten_block_product) = S ((S (S pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product)) /\ exists pa_q_hj32_row4_three_ten_block_product_successor. pa_u_hj32_row4_three_ten_block_product = pa_q_hj32_row4_three_ten_block_product_successor * S ((S (S pa_i_hj32_row4_three_ten_block_product)) * pa_v_hj32_row4_three_ten_block_product) + (pa_s_hj32_row4_three_ten_block_product))) /\ pa_s_hj32_row4_three_ten_block_product = pa_r_hj32_row4_three_ten_block_product * pa_p_hj32_row4_three_ten_block_product)))))))
34. 0034have hthree_ten_exponent : 5 * 2 = 10
35. 0035norm_num
36. 0036rewrite hthree_ten_exponent
37. 0037rewrite hthree_ten_exponent
38. 0038rewrite hthree_ten_exponent
39. 0039rewrite hthree_ten_exponent
40. 0040exact hthree_ten_witness
41. 0041have hfour_eight_block : exists pa_b_hj32_row4_four_eight_block pa_c_hj32_row4_four_eight_block. ((forall pa_i_hj32_row4_four_eight_block_repeat. (exists pa_lt_hj32_row4_four_eight_block_repeat_bound. pa_lt_hj32_row4_four_eight_block_repeat_bound + S pa_i_hj32_row4_four_eight_block_repeat = 4 * 2) -> (((exists pa_h_hj32_row4_four_eight_block_repeat_decoded. pa_h_hj32_row4_four_eight_block_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_eight_block_repeat)) * pa_c_hj32_row4_four_eight_block)) /\ exists pa_q_hj32_row4_four_eight_block_repeat_decoded. pa_b_hj32_row4_four_eight_block = pa_q_hj32_row4_four_eight_block_repeat_decoded * S ((S (pa_i_hj32_row4_four_eight_block_repeat)) * pa_c_hj32_row4_four_eight_block) + (4)))) /\ (exists pa_u_hj32_row4_four_eight_block_product pa_v_hj32_row4_four_eight_block_product. ((((exists pa_h_hj32_row4_four_eight_block_product_start. pa_h_hj32_row4_four_eight_block_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_start. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_start * S ((S (0)) * pa_v_hj32_row4_four_eight_block_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_terminal. pa_h_hj32_row4_four_eight_block_product_terminal + S (x4) = S ((S (4 * 2)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_terminal. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_terminal * S ((S (4 * 2)) * pa_v_hj32_row4_four_eight_block_product) + (x4))) /\ forall pa_i_hj32_row4_four_eight_block_product. (exists pa_lt_hj32_row4_four_eight_block_product_bound. pa_lt_hj32_row4_four_eight_block_product_bound + S pa_i_hj32_row4_four_eight_block_product = 4 * 2) -> exists pa_p_hj32_row4_four_eight_block_product pa_r_hj32_row4_four_eight_block_product pa_s_hj32_row4_four_eight_block_product. ((((exists pa_h_hj32_row4_four_eight_block_product_factor. pa_h_hj32_row4_four_eight_block_product_factor + S (pa_p_hj32_row4_four_eight_block_product) = S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_c_hj32_row4_four_eight_block)) /\ exists pa_q_hj32_row4_four_eight_block_product_factor. pa_b_hj32_row4_four_eight_block = pa_q_hj32_row4_four_eight_block_product_factor * S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_c_hj32_row4_four_eight_block) + (pa_p_hj32_row4_four_eight_block_product))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_partial. pa_h_hj32_row4_four_eight_block_product_partial + S (pa_r_hj32_row4_four_eight_block_product) = S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_partial. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_partial * S ((S (pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product) + (pa_r_hj32_row4_four_eight_block_product))) /\ ((((exists pa_h_hj32_row4_four_eight_block_product_successor. pa_h_hj32_row4_four_eight_block_product_successor + S (pa_s_hj32_row4_four_eight_block_product) = S ((S (S pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product)) /\ exists pa_q_hj32_row4_four_eight_block_product_successor. pa_u_hj32_row4_four_eight_block_product = pa_q_hj32_row4_four_eight_block_product_successor * S ((S (S pa_i_hj32_row4_four_eight_block_product)) * pa_v_hj32_row4_four_eight_block_product) + (pa_s_hj32_row4_four_eight_block_product))) /\ pa_s_hj32_row4_four_eight_block_product = pa_r_hj32_row4_four_eight_block_product * pa_p_hj32_row4_four_eight_block_product)))))))
42. 0042have hfour_eight_exponent : 4 * 2 = 8
43. 0043norm_num
44. 0044rewrite hfour_eight_exponent
45. 0045rewrite hfour_eight_exponent
46. 0046rewrite hfour_eight_exponent
47. 0047rewrite hfour_eight_exponent
48. 0048exact hfour_eight_witness
49. 0049have hblock : exists bqb_le_gap_hj32_row4_block_bound. bqb_le_gap_hj32_row4_block_bound + (x3) = (x4)
50. 0050specialize pow_block_bound_from_total 3
51. 0051specialize pow_block_bound_from_total 4
52. 0052specialize pow_block_bound_from_total 5
53. 0053specialize pow_block_bound_from_total 4
54. 0054specialize pow_block_bound_from_total 2
55. 0055specialize pow_block_bound_from_total x1
56. 0056specialize pow_block_bound_from_total x2
57. 0057specialize pow_block_bound_from_total x3
58. 0058specialize pow_block_bound_from_total x4
59. 0059apply pow_block_bound_from_total
60. 0060exact htotal
61. 0061exact hthree_five_witness
62. 0062exact hfour_four_witness
63. 0063exact hseed
64. 0064exact hthree_ten_block
65. 0065exact hfour_eight_block
66. 0066have htwo_ten : exists q. (exists pa_b_hj32_row4_two_ten pa_c_hj32_row4_two_ten. ((forall pa_i_hj32_row4_two_ten_repeat. (exists pa_lt_hj32_row4_two_ten_repeat_bound. pa_lt_hj32_row4_two_ten_repeat_bound + S pa_i_hj32_row4_two_ten_repeat = 10) -> (((exists pa_h_hj32_row4_two_ten_repeat_decoded. pa_h_hj32_row4_two_ten_repeat_decoded + S (2) = S ((S (pa_i_hj32_row4_two_ten_repeat)) * pa_c_hj32_row4_two_ten)) /\ exists pa_q_hj32_row4_two_ten_repeat_decoded. pa_b_hj32_row4_two_ten = pa_q_hj32_row4_two_ten_repeat_decoded * S ((S (pa_i_hj32_row4_two_ten_repeat)) * pa_c_hj32_row4_two_ten) + (2)))) /\ (exists pa_u_hj32_row4_two_ten_product pa_v_hj32_row4_two_ten_product. ((((exists pa_h_hj32_row4_two_ten_product_start. pa_h_hj32_row4_two_ten_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_start. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_start * S ((S (0)) * pa_v_hj32_row4_two_ten_product) + (1))) /\ ((((exists pa_h_hj32_row4_two_ten_product_terminal. pa_h_hj32_row4_two_ten_product_terminal + S (q) = S ((S (10)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_terminal. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_terminal * S ((S (10)) * pa_v_hj32_row4_two_ten_product) + (q))) /\ forall pa_i_hj32_row4_two_ten_product. (exists pa_lt_hj32_row4_two_ten_product_bound. pa_lt_hj32_row4_two_ten_product_bound + S pa_i_hj32_row4_two_ten_product = 10) -> exists pa_p_hj32_row4_two_ten_product pa_r_hj32_row4_two_ten_product pa_s_hj32_row4_two_ten_product. ((((exists pa_h_hj32_row4_two_ten_product_factor. pa_h_hj32_row4_two_ten_product_factor + S (pa_p_hj32_row4_two_ten_product) = S ((S (pa_i_hj32_row4_two_ten_product)) * pa_c_hj32_row4_two_ten)) /\ exists pa_q_hj32_row4_two_ten_product_factor. pa_b_hj32_row4_two_ten = pa_q_hj32_row4_two_ten_product_factor * S ((S (pa_i_hj32_row4_two_ten_product)) * pa_c_hj32_row4_two_ten) + (pa_p_hj32_row4_two_ten_product))) /\ ((((exists pa_h_hj32_row4_two_ten_product_partial. pa_h_hj32_row4_two_ten_product_partial + S (pa_r_hj32_row4_two_ten_product) = S ((S (pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_partial. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_partial * S ((S (pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product) + (pa_r_hj32_row4_two_ten_product))) /\ ((((exists pa_h_hj32_row4_two_ten_product_successor. pa_h_hj32_row4_two_ten_product_successor + S (pa_s_hj32_row4_two_ten_product) = S ((S (S pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product)) /\ exists pa_q_hj32_row4_two_ten_product_successor. pa_u_hj32_row4_two_ten_product = pa_q_hj32_row4_two_ten_product_successor * S ((S (S pa_i_hj32_row4_two_ten_product)) * pa_v_hj32_row4_two_ten_product) + (pa_s_hj32_row4_two_ten_product))) /\ pa_s_hj32_row4_two_ten_product = pa_r_hj32_row4_two_ten_product * pa_p_hj32_row4_two_ten_product))))))))
67. 0067specialize htotal 2
68. 0068specialize htotal 10
69. 0069exact htotal
70. 0070cases htwo_ten
71. 0071have hfour_five : exists q. (exists pa_b_hj32_row4_four_five pa_c_hj32_row4_four_five. ((forall pa_i_hj32_row4_four_five_repeat. (exists pa_lt_hj32_row4_four_five_repeat_bound. pa_lt_hj32_row4_four_five_repeat_bound + S pa_i_hj32_row4_four_five_repeat = 5) -> (((exists pa_h_hj32_row4_four_five_repeat_decoded. pa_h_hj32_row4_four_five_repeat_decoded + S (4) = S ((S (pa_i_hj32_row4_four_five_repeat)) * pa_c_hj32_row4_four_five)) /\ exists pa_q_hj32_row4_four_five_repeat_decoded. pa_b_hj32_row4_four_five = pa_q_hj32_row4_four_five_repeat_decoded * S ((S (pa_i_hj32_row4_four_five_repeat)) * pa_c_hj32_row4_four_five) + (4)))) /\ (exists pa_u_hj32_row4_four_five_product pa_v_hj32_row4_four_five_product. ((((exists pa_h_hj32_row4_four_five_product_start. pa_h_hj32_row4_four_five_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_start. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_start * S ((S (0)) * pa_v_hj32_row4_four_five_product) + (1))) /\ ((((exists pa_h_hj32_row4_four_five_product_terminal. pa_h_hj32_row4_four_five_product_terminal + S (q) = S ((S (5)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_terminal. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_terminal * S ((S (5)) * pa_v_hj32_row4_four_five_product) + (q))) /\ forall pa_i_hj32_row4_four_five_product. (exists pa_lt_hj32_row4_four_five_product_bound. pa_lt_hj32_row4_four_five_product_bound + S pa_i_hj32_row4_four_five_product = 5) -> exists pa_p_hj32_row4_four_five_product pa_r_hj32_row4_four_five_product pa_s_hj32_row4_four_five_product. ((((exists pa_h_hj32_row4_four_five_product_factor. pa_h_hj32_row4_four_five_product_factor + S (pa_p_hj32_row4_four_five_product) = S ((S (pa_i_hj32_row4_four_five_product)) * pa_c_hj32_row4_four_five)) /\ exists pa_q_hj32_row4_four_five_product_factor. pa_b_hj32_row4_four_five = pa_q_hj32_row4_four_five_product_factor * S ((S (pa_i_hj32_row4_four_five_product)) * pa_c_hj32_row4_four_five) + (pa_p_hj32_row4_four_five_product))) /\ ((((exists pa_h_hj32_row4_four_five_product_partial. pa_h_hj32_row4_four_five_product_partial + S (pa_r_hj32_row4_four_five_product) = S ((S (pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_partial. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_partial * S ((S (pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product) + (pa_r_hj32_row4_four_five_product))) /\ ((((exists pa_h_hj32_row4_four_five_product_successor. pa_h_hj32_row4_four_five_product_successor + S (pa_s_hj32_row4_four_five_product) = S ((S (S pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product)) /\ exists pa_q_hj32_row4_four_five_product_successor. pa_u_hj32_row4_four_five_product = pa_q_hj32_row4_four_five_product_successor * S ((S (S pa_i_hj32_row4_four_five_product)) * pa_v_hj32_row4_four_five_product) + (pa_s_hj32_row4_four_five_product))) /\ pa_s_hj32_row4_four_five_product = pa_r_hj32_row4_four_five_product * pa_p_hj32_row4_four_five_product))))))))
72. 0072specialize htotal 4
73. 0073specialize htotal 5
74. 0074exact htotal
75. 0075cases hfour_five
76. 0076have hseeds : (exists pa_b_hj32_seed_two_two pa_c_hj32_seed_two_two. ((forall pa_i_hj32_seed_two_two_repeat. (exists pa_lt_hj32_seed_two_two_repeat_bound. pa_lt_hj32_seed_two_two_repeat_bound + S pa_i_hj32_seed_two_two_repeat = 2) -> (((exists pa_h_hj32_seed_two_two_repeat_decoded. pa_h_hj32_seed_two_two_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_repeat_decoded. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_repeat_decoded * S ((S (pa_i_hj32_seed_two_two_repeat)) * pa_c_hj32_seed_two_two) + (2)))) /\ (exists pa_u_hj32_seed_two_two_product pa_v_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_start. pa_h_hj32_seed_two_two_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_start. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_start * S ((S (0)) * pa_v_hj32_seed_two_two_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_two_product_terminal. pa_h_hj32_seed_two_two_product_terminal + S (4) = S ((S (2)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_terminal. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_terminal * S ((S (2)) * pa_v_hj32_seed_two_two_product) + (4))) /\ forall pa_i_hj32_seed_two_two_product. (exists pa_lt_hj32_seed_two_two_product_bound. pa_lt_hj32_seed_two_two_product_bound + S pa_i_hj32_seed_two_two_product = 2) -> exists pa_p_hj32_seed_two_two_product pa_r_hj32_seed_two_two_product pa_s_hj32_seed_two_two_product. ((((exists pa_h_hj32_seed_two_two_product_factor. pa_h_hj32_seed_two_two_product_factor + S (pa_p_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two)) /\ exists pa_q_hj32_seed_two_two_product_factor. pa_b_hj32_seed_two_two = pa_q_hj32_seed_two_two_product_factor * S ((S (pa_i_hj32_seed_two_two_product)) * pa_c_hj32_seed_two_two) + (pa_p_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_partial. pa_h_hj32_seed_two_two_product_partial + S (pa_r_hj32_seed_two_two_product) = S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_partial. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_partial * S ((S (pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_r_hj32_seed_two_two_product))) /\ ((((exists pa_h_hj32_seed_two_two_product_successor. pa_h_hj32_seed_two_two_product_successor + S (pa_s_hj32_seed_two_two_product) = S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product)) /\ exists pa_q_hj32_seed_two_two_product_successor. pa_u_hj32_seed_two_two_product = pa_q_hj32_seed_two_two_product_successor * S ((S (S pa_i_hj32_seed_two_two_product)) * pa_v_hj32_seed_two_two_product) + (pa_s_hj32_seed_two_two_product))) /\ pa_s_hj32_seed_two_two_product = pa_r_hj32_seed_two_two_product * pa_p_hj32_seed_two_two_product)))))))) /\ (exists pa_b_hj32_seed_two_seven pa_c_hj32_seed_two_seven. ((forall pa_i_hj32_seed_two_seven_repeat. (exists pa_lt_hj32_seed_two_seven_repeat_bound. pa_lt_hj32_seed_two_seven_repeat_bound + S pa_i_hj32_seed_two_seven_repeat = 7) -> (((exists pa_h_hj32_seed_two_seven_repeat_decoded. pa_h_hj32_seed_two_seven_repeat_decoded + S (2) = S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_repeat_decoded. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_repeat_decoded * S ((S (pa_i_hj32_seed_two_seven_repeat)) * pa_c_hj32_seed_two_seven) + (2)))) /\ (exists pa_u_hj32_seed_two_seven_product pa_v_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_start. pa_h_hj32_seed_two_seven_product_start + S (1) = S ((S (0)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_start. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_start * S ((S (0)) * pa_v_hj32_seed_two_seven_product) + (1))) /\ ((((exists pa_h_hj32_seed_two_seven_product_terminal. pa_h_hj32_seed_two_seven_product_terminal + S (128) = S ((S (7)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_terminal. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_terminal * S ((S (7)) * pa_v_hj32_seed_two_seven_product) + (128))) /\ forall pa_i_hj32_seed_two_seven_product. (exists pa_lt_hj32_seed_two_seven_product_bound. pa_lt_hj32_seed_two_seven_product_bound + S pa_i_hj32_seed_two_seven_product = 7) -> exists pa_p_hj32_seed_two_seven_product pa_r_hj32_seed_two_seven_product pa_s_hj32_seed_two_seven_product. ((((exists pa_h_hj32_seed_two_seven_product_factor. pa_h_hj32_seed_two_seven_product_factor + S (pa_p_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven)) /\ exists pa_q_hj32_seed_two_seven_product_factor. pa_b_hj32_seed_two_seven = pa_q_hj32_seed_two_seven_product_factor * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_c_hj32_seed_two_seven) + (pa_p_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_partial. pa_h_hj32_seed_two_seven_product_partial + S (pa_r_hj32_seed_two_seven_product) = S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_partial. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_partial * S ((S (pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_r_hj32_seed_two_seven_product))) /\ ((((exists pa_h_hj32_seed_two_seven_product_successor. pa_h_hj32_seed_two_seven_product_successor + S (pa_s_hj32_seed_two_seven_product) = S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product)) /\ exists pa_q_hj32_seed_two_seven_product_successor. pa_u_hj32_seed_two_seven_product = pa_q_hj32_seed_two_seven_product_successor * S ((S (S pa_i_hj32_seed_two_seven_product)) * pa_v_hj32_seed_two_seven_product) + (pa_s_hj32_seed_two_seven_product))) /\ pa_s_hj32_seed_two_seven_product = pa_r_hj32_seed_two_seven_product * pa_p_hj32_seed_two_seven_product))))))))
77. 0077apply pow_two_seed_bundle_from_total
78. 0078exact htotal
79. 0079cases hseeds
80. 0080have htwo_bridge : x6 = x5
81. 0081specialize pow_mul_exp_from_total 2
82. 0082specialize pow_mul_exp_from_total 2
83. 0083specialize pow_mul_exp_from_total 5
84. 0084specialize pow_mul_exp_from_total 10
85. 0085specialize pow_mul_exp_from_total 4
86. 0086specialize pow_mul_exp_from_total x6
87. 0087specialize pow_mul_exp_from_total x5
88. 0088apply pow_mul_exp_from_total
89. 0089exact htotal
90. 0090norm_num
91. 0091exact hseeds_left
92. 0092exact hfour_five_witness
93. 0093exact htwo_ten_witness
94. 0094have hxfactor : exists pa_b_hj32_row4_six_factor pa_c_hj32_row4_six_factor. ((forall pa_i_hj32_row4_six_factor_repeat. (exists pa_lt_hj32_row4_six_factor_repeat_bound. pa_lt_hj32_row4_six_factor_repeat_bound + S pa_i_hj32_row4_six_factor_repeat = 10) -> (((exists pa_h_hj32_row4_six_factor_repeat_decoded. pa_h_hj32_row4_six_factor_repeat_decoded + S (2 * 3) = S ((S (pa_i_hj32_row4_six_factor_repeat)) * pa_c_hj32_row4_six_factor)) /\ exists pa_q_hj32_row4_six_factor_repeat_decoded. pa_b_hj32_row4_six_factor = pa_q_hj32_row4_six_factor_repeat_decoded * S ((S (pa_i_hj32_row4_six_factor_repeat)) * pa_c_hj32_row4_six_factor) + (2 * 3)))) /\ (exists pa_u_hj32_row4_six_factor_product pa_v_hj32_row4_six_factor_product. ((((exists pa_h_hj32_row4_six_factor_product_start. pa_h_hj32_row4_six_factor_product_start + S (1) = S ((S (0)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_start. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_start * S ((S (0)) * pa_v_hj32_row4_six_factor_product) + (1))) /\ ((((exists pa_h_hj32_row4_six_factor_product_terminal. pa_h_hj32_row4_six_factor_product_terminal + S (x) = S ((S (10)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_terminal. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_terminal * S ((S (10)) * pa_v_hj32_row4_six_factor_product) + (x))) /\ forall pa_i_hj32_row4_six_factor_product. (exists pa_lt_hj32_row4_six_factor_product_bound. pa_lt_hj32_row4_six_factor_product_bound + S pa_i_hj32_row4_six_factor_product = 10) -> exists pa_p_hj32_row4_six_factor_product pa_r_hj32_row4_six_factor_product pa_s_hj32_row4_six_factor_product. ((((exists pa_h_hj32_row4_six_factor_product_factor. pa_h_hj32_row4_six_factor_product_factor + S (pa_p_hj32_row4_six_factor_product) = S ((S (pa_i_hj32_row4_six_factor_product)) * pa_c_hj32_row4_six_factor)) /\ exists pa_q_hj32_row4_six_factor_product_factor. pa_b_hj32_row4_six_factor = pa_q_hj32_row4_six_factor_product_factor * S ((S (pa_i_hj32_row4_six_factor_product)) * pa_c_hj32_row4_six_factor) + (pa_p_hj32_row4_six_factor_product))) /\ ((((exists pa_h_hj32_row4_six_factor_product_partial. pa_h_hj32_row4_six_factor_product_partial + S (pa_r_hj32_row4_six_factor_product) = S ((S (pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_partial. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_partial * S ((S (pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product) + (pa_r_hj32_row4_six_factor_product))) /\ ((((exists pa_h_hj32_row4_six_factor_product_successor. pa_h_hj32_row4_six_factor_product_successor + S (pa_s_hj32_row4_six_factor_product) = S ((S (S pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product)) /\ exists pa_q_hj32_row4_six_factor_product_successor. pa_u_hj32_row4_six_factor_product = pa_q_hj32_row4_six_factor_product_successor * S ((S (S pa_i_hj32_row4_six_factor_product)) * pa_v_hj32_row4_six_factor_product) + (pa_s_hj32_row4_six_factor_product))) /\ pa_s_hj32_row4_six_factor_product = pa_r_hj32_row4_six_factor_product * pa_p_hj32_row4_six_factor_product)))))))
95. 0095have hsix : 2 * 3 = 6
96. 0096norm_num
97. 0097rewrite hsix
98. 0098rewrite hsix
99. 0099exact hx
100. 0100have hxproduct : x = x5 * x3
101. 0101specialize pow_mul_base 2
102. 0102specialize pow_mul_base 3
103. 0103specialize pow_mul_base 10
104. 0104specialize pow_mul_base x5
105. 0105specialize pow_mul_base x3
106. 0106specialize pow_mul_base x
107. 0107apply pow_mul_base
108. 0108exact htwo_ten_witness
109. 0109exact hthree_ten_witness
110. 0110exact hxfactor
111. 0111have hyproduct : y = x6 * x4
112. 0112specialize pow_add 4
113. 0113specialize pow_add 5
114. 0114specialize pow_add 8
115. 0115specialize pow_add 13
116. 0116specialize pow_add x6
117. 0117specialize pow_add x4
118. 0118specialize pow_add y
119. 0119apply pow_add
120. 0120norm_num
121. 0121exact hfour_five_witness
122. 0122exact hfour_eight_witness
123. 0123exact hy
124. 0124rewrite htwo_bridge at hyproduct
125. 0125have hfactor_bound : exists bqb_le_gap_hj32_row4_product_bound. bqb_le_gap_hj32_row4_product_bound + (x5 * x3) = (x5 * x4)
126. 0126specialize mul_le_mul x5
127. 0127specialize mul_le_mul x5
128. 0128specialize mul_le_mul x3
129. 0129specialize mul_le_mul x4
130. 0130apply mul_le_mul
131. 0131specialize le_refl x5
132. 0132exact le_refl
133. 0133exact hblock
134. 0134rewrite <- hxproduct at hfactor_bound
135. 0135rewrite <- hyproduct at hfactor_bound
136. 0136exact hfactor_bound