gauss_lemma_power_congruence_exists

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

1. 0001intro p
2. 0002intro h
3. 0003intro a
4. 0004intro b
5. 0005intro c
6. 0006intro hpodd
7. 0007intro hprime
8. 0008intro hnotdiv
9. 0009intro hhalf
10. 0010have hpsucc : p = S (2 * h)
11. 0011trans 2 * h + 1
12. 0012exact hpodd
13. 0013simp
14. 0014have hsigned_exists : exists mb mc sb sc. (forall gsp_index_lemma_endpoint_signed_prefix. (exists gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound. gsp_lt_gap_lemma_endpoint_signed_prefix_index_bound + S gsp_index_lemma_endpoint_signed_prefix = h) -> (exists gsp_value_lemma_endpoint_signed_prefix_entry gsp_magnitude_lemma_endpoint_signed_prefix_entry gsp_sign_lemma_endpoint_signed_prefix_entry. (((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_source. ff_h_gsp_lemma_endpoint_signed_prefix_entry_source + S (gsp_value_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_source. b = ff_q_gsp_lemma_endpoint_signed_prefix_entry_source * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * c) + (gsp_value_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude. ff_h_gsp_lemma_endpoint_signed_prefix_entry_magnitude + S (gsp_magnitude_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude. mb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_magnitude * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * mc) + (gsp_magnitude_lemma_endpoint_signed_prefix_entry))) /\ ((((exists ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign. ff_h_gsp_lemma_endpoint_signed_prefix_entry_sign + S (gsp_sign_lemma_endpoint_signed_prefix_entry) = S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc)) /\ exists ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign. sb = ff_q_gsp_lemma_endpoint_signed_prefix_entry_sign * S ((S (gsp_index_lemma_endpoint_signed_prefix)) * sc) + (gsp_sign_lemma_endpoint_signed_prefix_entry))) /\ ((exists gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive. gsp_lt_gap_lemma_endpoint_signed_prefix_entry_positive + S 0 = gsp_magnitude_lemma_endpoint_signed_prefix_entry) /\ ((exists gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded. gsp_le_gap_lemma_endpoint_signed_prefix_entry_bounded + gsp_magnitude_lemma_endpoint_signed_prefix_entry = h) /\ ((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 \/ gsp_sign_lemma_endpoint_signed_prefix_entry = 1) /\ (((gsp_sign_lemma_endpoint_signed_prefix_entry = 0 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_lower = (gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_lower)) \/ (gsp_sign_lemma_endpoint_signed_prefix_entry = 1 /\ (exists gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected. (a * gsp_value_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_left_lemma_endpoint_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_lemma_endpoint_signed_prefix_entry) + p * gsp_mod_right_lemma_endpoint_signed_prefix_entry_reflected)))))))))))
15. 0015specialize gauss_half_range_signed_prefix_exists p
16. 0016specialize gauss_half_range_signed_prefix_exists h
17. 0017specialize gauss_half_range_signed_prefix_exists a
18. 0018specialize gauss_half_range_signed_prefix_exists b
19. 0019specialize gauss_half_range_signed_prefix_exists c
20. 0020apply gauss_half_range_signed_prefix_exists
21. 0021exact hpodd
22. 0022exact hprime
23. 0023exact hnotdiv
24. 0024exact hhalf
25. 0025cases hsigned_exists
26. 0026cases hsigned_exists_witness
27. 0027cases hsigned_exists_witness_witness
28. 0028cases hsigned_exists_witness_witness_witness
29. 0029have hcount_exists : exists e. (((exists ff_u_lemma_endpoint_local_bit_count_sum ff_v_lemma_endpoint_local_bit_count_sum. ((((exists ff_h_lemma_endpoint_local_bit_count_sum_start. ff_h_lemma_endpoint_local_bit_count_sum_start + S (0) = S ((S (0)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_start. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_start * S ((S (0)) * ff_v_lemma_endpoint_local_bit_count_sum) + (0))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_terminal. ff_h_lemma_endpoint_local_bit_count_sum_terminal + S (e) = S ((S (h)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_terminal. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_terminal * S ((S (h)) * ff_v_lemma_endpoint_local_bit_count_sum) + (e))) /\ forall ff_i_lemma_endpoint_local_bit_count_sum. (exists ff_lt_lemma_endpoint_local_bit_count_sum_bound. ff_lt_lemma_endpoint_local_bit_count_sum_bound + S ff_i_lemma_endpoint_local_bit_count_sum = h) -> exists ff_a_lemma_endpoint_local_bit_count_sum ff_r_lemma_endpoint_local_bit_count_sum ff_s_lemma_endpoint_local_bit_count_sum. ((((exists ff_h_lemma_endpoint_local_bit_count_sum_summand. ff_h_lemma_endpoint_local_bit_count_sum_summand + S (ff_a_lemma_endpoint_local_bit_count_sum) = S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * x3)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_summand. x2 = ff_q_lemma_endpoint_local_bit_count_sum_summand * S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * x3) + (ff_a_lemma_endpoint_local_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_partial. ff_h_lemma_endpoint_local_bit_count_sum_partial + S (ff_r_lemma_endpoint_local_bit_count_sum) = S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_partial. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_partial * S ((S (ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum) + (ff_r_lemma_endpoint_local_bit_count_sum))) /\ ((((exists ff_h_lemma_endpoint_local_bit_count_sum_successor. ff_h_lemma_endpoint_local_bit_count_sum_successor + S (ff_s_lemma_endpoint_local_bit_count_sum) = S ((S (S ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum)) /\ exists ff_q_lemma_endpoint_local_bit_count_sum_successor. ff_u_lemma_endpoint_local_bit_count_sum = ff_q_lemma_endpoint_local_bit_count_sum_successor * S ((S (S ff_i_lemma_endpoint_local_bit_count_sum)) * ff_v_lemma_endpoint_local_bit_count_sum) + (ff_s_lemma_endpoint_local_bit_count_sum))) /\ ff_s_lemma_endpoint_local_bit_count_sum = ff_r_lemma_endpoint_local_bit_count_sum + ff_a_lemma_endpoint_local_bit_count_sum)))))) /\ (forall ff_i_lemma_endpoint_local_bit_count_bits. (exists ff_lt_lemma_endpoint_local_bit_count_bits_bound. ff_lt_lemma_endpoint_local_bit_count_bits_bound + S ff_i_lemma_endpoint_local_bit_count_bits = h) -> exists ff_bit_lemma_endpoint_local_bit_count_bits. ((((exists ff_h_lemma_endpoint_local_bit_count_bits_decoded. ff_h_lemma_endpoint_local_bit_count_bits_decoded + S (ff_bit_lemma_endpoint_local_bit_count_bits) = S ((S (ff_i_lemma_endpoint_local_bit_count_bits)) * x3)) /\ exists ff_q_lemma_endpoint_local_bit_count_bits_decoded. x2 = ff_q_lemma_endpoint_local_bit_count_bits_decoded * S ((S (ff_i_lemma_endpoint_local_bit_count_bits)) * x3) + (ff_bit_lemma_endpoint_local_bit_count_bits))) /\ (ff_bit_lemma_endpoint_local_bit_count_bits = 0 \/ ff_bit_lemma_endpoint_local_bit_count_bits = 1)))))
30. 0030specialize gauss_signed_half_bit_count_exists p
31. 0031specialize gauss_signed_half_bit_count_exists h
32. 0032specialize gauss_signed_half_bit_count_exists a
33. 0033specialize gauss_signed_half_bit_count_exists b
34. 0034specialize gauss_signed_half_bit_count_exists c
35. 0035specialize gauss_signed_half_bit_count_exists x
36. 0036specialize gauss_signed_half_bit_count_exists x1
37. 0037specialize gauss_signed_half_bit_count_exists x2
38. 0038specialize gauss_signed_half_bit_count_exists x3
39. 0039specialize gauss_signed_half_bit_count_exists h
40. 0040apply gauss_signed_half_bit_count_exists
41. 0041exact hsigned_exists_witness_witness_witness_witness
42. 0042cases hcount_exists
43. 0043have hmagnitude_range : forall gmp_index_lemma_endpoint_magnitude_range. (exists gsp_lt_gap_lemma_endpoint_magnitude_range_index_bound. gsp_lt_gap_lemma_endpoint_magnitude_range_index_bound + S gmp_index_lemma_endpoint_magnitude_range = h) -> exists gmp_magnitude_lemma_endpoint_magnitude_range. ((((exists ff_h_gmp_lemma_endpoint_magnitude_range_decoded. ff_h_gmp_lemma_endpoint_magnitude_range_decoded + S (gmp_magnitude_lemma_endpoint_magnitude_range) = S ((S (gmp_index_lemma_endpoint_magnitude_range)) * x1)) /\ exists ff_q_gmp_lemma_endpoint_magnitude_range_decoded. x = ff_q_gmp_lemma_endpoint_magnitude_range_decoded * S ((S (gmp_index_lemma_endpoint_magnitude_range)) * x1) + (gmp_magnitude_lemma_endpoint_magnitude_range))) /\ ((exists gsp_lt_gap_lemma_endpoint_magnitude_range_positive. gsp_lt_gap_lemma_endpoint_magnitude_range_positive + S 0 = gmp_magnitude_lemma_endpoint_magnitude_range) /\ (exists gsp_le_gap_lemma_endpoint_magnitude_range_bounded. gsp_le_gap_lemma_endpoint_magnitude_range_bounded + gmp_magnitude_lemma_endpoint_magnitude_range = h)))
44. 0044specialize gauss_signed_half_magnitude_range p
45. 0045specialize gauss_signed_half_magnitude_range h
46. 0046specialize gauss_signed_half_magnitude_range a
47. 0047specialize gauss_signed_half_magnitude_range b
48. 0048specialize gauss_signed_half_magnitude_range c
49. 0049specialize gauss_signed_half_magnitude_range x
50. 0050specialize gauss_signed_half_magnitude_range x1
51. 0051specialize gauss_signed_half_magnitude_range x2
52. 0052specialize gauss_signed_half_magnitude_range x3
53. 0053specialize gauss_signed_half_magnitude_range h
54. 0054apply gauss_signed_half_magnitude_range
55. 0055exact hsigned_exists_witness_witness_witness_witness
56. 0056have hmagnitude_injective : forall fp_i_lemma_endpoint_magnitude_injective fp_j_lemma_endpoint_magnitude_injective fp_value_lemma_endpoint_magnitude_injective. (exists fp_gap_lemma_endpoint_magnitude_injective_i. fp_gap_lemma_endpoint_magnitude_injective_i + S fp_i_lemma_endpoint_magnitude_injective = h) -> (exists fp_gap_lemma_endpoint_magnitude_injective_j. fp_gap_lemma_endpoint_magnitude_injective_j + S fp_j_lemma_endpoint_magnitude_injective = h) -> (((exists ff_h_lemma_endpoint_magnitude_injective_left. ff_h_lemma_endpoint_magnitude_injective_left + S (fp_value_lemma_endpoint_magnitude_injective) = S ((S (fp_i_lemma_endpoint_magnitude_injective)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_injective_left. x = ff_q_lemma_endpoint_magnitude_injective_left * S ((S (fp_i_lemma_endpoint_magnitude_injective)) * x1) + (fp_value_lemma_endpoint_magnitude_injective))) -> (((exists ff_h_lemma_endpoint_magnitude_injective_right. ff_h_lemma_endpoint_magnitude_injective_right + S (fp_value_lemma_endpoint_magnitude_injective) = S ((S (fp_j_lemma_endpoint_magnitude_injective)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_injective_right. x = ff_q_lemma_endpoint_magnitude_injective_right * S ((S (fp_j_lemma_endpoint_magnitude_injective)) * x1) + (fp_value_lemma_endpoint_magnitude_injective))) -> fp_i_lemma_endpoint_magnitude_injective = fp_j_lemma_endpoint_magnitude_injective
57. 0057specialize gauss_signed_half_magnitude_injective p
58. 0058specialize gauss_signed_half_magnitude_injective h
59. 0059specialize gauss_signed_half_magnitude_injective a
60. 0060specialize gauss_signed_half_magnitude_injective b
61. 0061specialize gauss_signed_half_magnitude_injective c
62. 0062specialize gauss_signed_half_magnitude_injective x
63. 0063specialize gauss_signed_half_magnitude_injective x1
64. 0064specialize gauss_signed_half_magnitude_injective x2
65. 0065specialize gauss_signed_half_magnitude_injective x3
66. 0066apply gauss_signed_half_magnitude_injective
67. 0067exact hpodd
68. 0068exact hprime
69. 0069exact hnotdiv
70. 0070exact hhalf
71. 0071exact hsigned_exists_witness_witness_witness_witness
72. 0072have hrecode_exists : exists rb rc. (forall gmp_index_lemma_endpoint_predecessor_recode gmp_predecessor_lemma_endpoint_predecessor_recode. (exists gsp_lt_gap_lemma_endpoint_predecessor_recode_index_bound. gsp_lt_gap_lemma_endpoint_predecessor_recode_index_bound + S gmp_index_lemma_endpoint_predecessor_recode = h) -> (((exists gsp_beta_height_gmp_lemma_endpoint_predecessor_recode_source. gsp_beta_height_gmp_lemma_endpoint_predecessor_recode_source + S (S gmp_predecessor_lemma_endpoint_predecessor_recode) = S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * x1)) /\ exists gsp_beta_quotient_gmp_lemma_endpoint_predecessor_recode_source. x = gsp_beta_quotient_gmp_lemma_endpoint_predecessor_recode_source * S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * x1) + (S gmp_predecessor_lemma_endpoint_predecessor_recode))) -> (((exists ff_h_gmp_lemma_endpoint_predecessor_recode_target. ff_h_gmp_lemma_endpoint_predecessor_recode_target + S (gmp_predecessor_lemma_endpoint_predecessor_recode) = S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * rc)) /\ exists ff_q_gmp_lemma_endpoint_predecessor_recode_target. rb = ff_q_gmp_lemma_endpoint_predecessor_recode_target * S ((S (gmp_index_lemma_endpoint_predecessor_recode)) * rc) + (gmp_predecessor_lemma_endpoint_predecessor_recode))))
73. 0073specialize gauss_signed_half_predecessor_recode_exists p
74. 0074specialize gauss_signed_half_predecessor_recode_exists h
75. 0075specialize gauss_signed_half_predecessor_recode_exists a
76. 0076specialize gauss_signed_half_predecessor_recode_exists b
77. 0077specialize gauss_signed_half_predecessor_recode_exists c
78. 0078specialize gauss_signed_half_predecessor_recode_exists x
79. 0079specialize gauss_signed_half_predecessor_recode_exists x1
80. 0080specialize gauss_signed_half_predecessor_recode_exists x2
81. 0081specialize gauss_signed_half_predecessor_recode_exists x3
82. 0082apply gauss_signed_half_predecessor_recode_exists
83. 0083exact hsigned_exists_witness_witness_witness_witness
84. 0084cases hrecode_exists
85. 0085cases hrecode_exists_witness
86. 0086have hcanonical_product_exists : exists P. (exists ff_u_lemma_endpoint_canonical_product ff_v_lemma_endpoint_canonical_product. ((((exists ff_h_lemma_endpoint_canonical_product_start. ff_h_lemma_endpoint_canonical_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_start. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_start * S ((S (0)) * ff_v_lemma_endpoint_canonical_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_terminal. ff_h_lemma_endpoint_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_terminal. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_canonical_product) + (P))) /\ forall ff_i_lemma_endpoint_canonical_product. (exists ff_lt_lemma_endpoint_canonical_product_bound. ff_lt_lemma_endpoint_canonical_product_bound + S ff_i_lemma_endpoint_canonical_product = h) -> exists ff_p_lemma_endpoint_canonical_product ff_r_lemma_endpoint_canonical_product ff_s_lemma_endpoint_canonical_product. ((((exists ff_h_lemma_endpoint_canonical_product_factor. ff_h_lemma_endpoint_canonical_product_factor + S (ff_p_lemma_endpoint_canonical_product) = S ((S (ff_i_lemma_endpoint_canonical_product)) * c)) /\ exists ff_q_lemma_endpoint_canonical_product_factor. b = ff_q_lemma_endpoint_canonical_product_factor * S ((S (ff_i_lemma_endpoint_canonical_product)) * c) + (ff_p_lemma_endpoint_canonical_product))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_partial. ff_h_lemma_endpoint_canonical_product_partial + S (ff_r_lemma_endpoint_canonical_product) = S ((S (ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_partial. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_partial * S ((S (ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product) + (ff_r_lemma_endpoint_canonical_product))) /\ ((((exists ff_h_lemma_endpoint_canonical_product_successor. ff_h_lemma_endpoint_canonical_product_successor + S (ff_s_lemma_endpoint_canonical_product) = S ((S (S ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product)) /\ exists ff_q_lemma_endpoint_canonical_product_successor. ff_u_lemma_endpoint_canonical_product = ff_q_lemma_endpoint_canonical_product_successor * S ((S (S ff_i_lemma_endpoint_canonical_product)) * ff_v_lemma_endpoint_canonical_product) + (ff_s_lemma_endpoint_canonical_product))) /\ ff_s_lemma_endpoint_canonical_product = ff_r_lemma_endpoint_canonical_product * ff_p_lemma_endpoint_canonical_product))))))
87. 0087specialize beta_product_exists b
88. 0088specialize beta_product_exists c
89. 0089specialize beta_product_exists h
90. 0090exact beta_product_exists
91. 0091cases hcanonical_product_exists
92. 0092have hmagnitude_product_exists : exists M. (exists ff_u_lemma_endpoint_magnitude_product ff_v_lemma_endpoint_magnitude_product. ((((exists ff_h_lemma_endpoint_magnitude_product_start. ff_h_lemma_endpoint_magnitude_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_start. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_start * S ((S (0)) * ff_v_lemma_endpoint_magnitude_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_terminal. ff_h_lemma_endpoint_magnitude_product_terminal + S (M) = S ((S (h)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_terminal. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_magnitude_product) + (M))) /\ forall ff_i_lemma_endpoint_magnitude_product. (exists ff_lt_lemma_endpoint_magnitude_product_bound. ff_lt_lemma_endpoint_magnitude_product_bound + S ff_i_lemma_endpoint_magnitude_product = h) -> exists ff_p_lemma_endpoint_magnitude_product ff_r_lemma_endpoint_magnitude_product ff_s_lemma_endpoint_magnitude_product. ((((exists ff_h_lemma_endpoint_magnitude_product_factor. ff_h_lemma_endpoint_magnitude_product_factor + S (ff_p_lemma_endpoint_magnitude_product) = S ((S (ff_i_lemma_endpoint_magnitude_product)) * x1)) /\ exists ff_q_lemma_endpoint_magnitude_product_factor. x = ff_q_lemma_endpoint_magnitude_product_factor * S ((S (ff_i_lemma_endpoint_magnitude_product)) * x1) + (ff_p_lemma_endpoint_magnitude_product))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_partial. ff_h_lemma_endpoint_magnitude_product_partial + S (ff_r_lemma_endpoint_magnitude_product) = S ((S (ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_partial. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_partial * S ((S (ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product) + (ff_r_lemma_endpoint_magnitude_product))) /\ ((((exists ff_h_lemma_endpoint_magnitude_product_successor. ff_h_lemma_endpoint_magnitude_product_successor + S (ff_s_lemma_endpoint_magnitude_product) = S ((S (S ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product)) /\ exists ff_q_lemma_endpoint_magnitude_product_successor. ff_u_lemma_endpoint_magnitude_product = ff_q_lemma_endpoint_magnitude_product_successor * S ((S (S ff_i_lemma_endpoint_magnitude_product)) * ff_v_lemma_endpoint_magnitude_product) + (ff_s_lemma_endpoint_magnitude_product))) /\ ff_s_lemma_endpoint_magnitude_product = ff_r_lemma_endpoint_magnitude_product * ff_p_lemma_endpoint_magnitude_product))))))
93. 0093specialize beta_product_exists x
94. 0094specialize beta_product_exists x1
95. 0095specialize beta_product_exists h
96. 0096exact beta_product_exists
97. 0097cases hmagnitude_product_exists
98. 0098have hsign_package : exists fb fc Sprod R. ((forall gspf_index_lemma_endpoint_sign_factors_expanded gspf_bit_lemma_endpoint_sign_factors_expanded. (exists gsp_lt_gap_lemma_endpoint_sign_factors_expanded_bound. gsp_lt_gap_lemma_endpoint_sign_factors_expanded_bound + S gspf_index_lemma_endpoint_sign_factors_expanded = h) -> (((exists ff_h_gspf_lemma_endpoint_sign_factors_expanded_bit. ff_h_gspf_lemma_endpoint_sign_factors_expanded_bit + S (gspf_bit_lemma_endpoint_sign_factors_expanded) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * x3)) /\ exists ff_q_gspf_lemma_endpoint_sign_factors_expanded_bit. x2 = ff_q_gspf_lemma_endpoint_sign_factors_expanded_bit * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * x3) + (gspf_bit_lemma_endpoint_sign_factors_expanded))) -> (((gspf_bit_lemma_endpoint_sign_factors_expanded = 0) /\ (((exists gsp_beta_height_gspf_lemma_endpoint_sign_factors_expanded_one. gsp_beta_height_gspf_lemma_endpoint_sign_factors_expanded_one + S (1) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc)) /\ exists gsp_beta_quotient_gspf_lemma_endpoint_sign_factors_expanded_one. fb = gsp_beta_quotient_gspf_lemma_endpoint_sign_factors_expanded_one * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc) + (1)))) \/ ((gspf_bit_lemma_endpoint_sign_factors_expanded = 1) /\ (((exists ff_h_gspf_lemma_endpoint_sign_factors_expanded_predecessor. ff_h_gspf_lemma_endpoint_sign_factors_expanded_predecessor + S ((2 * h)) = S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc)) /\ exists ff_q_gspf_lemma_endpoint_sign_factors_expanded_predecessor. fb = ff_q_gspf_lemma_endpoint_sign_factors_expanded_predecessor * S ((S (gspf_index_lemma_endpoint_sign_factors_expanded)) * fc) + ((2 * h))))))) /\ ((exists ff_u_lemma_endpoint_sign_product ff_v_lemma_endpoint_sign_product. ((((exists ff_h_lemma_endpoint_sign_product_start. ff_h_lemma_endpoint_sign_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_start. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_start * S ((S (0)) * ff_v_lemma_endpoint_sign_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_sign_product_terminal. ff_h_lemma_endpoint_sign_product_terminal + S (Sprod) = S ((S (h)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_terminal. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_sign_product) + (Sprod))) /\ forall ff_i_lemma_endpoint_sign_product. (exists ff_lt_lemma_endpoint_sign_product_bound. ff_lt_lemma_endpoint_sign_product_bound + S ff_i_lemma_endpoint_sign_product = h) -> exists ff_p_lemma_endpoint_sign_product ff_r_lemma_endpoint_sign_product ff_s_lemma_endpoint_sign_product. ((((exists ff_h_lemma_endpoint_sign_product_factor. ff_h_lemma_endpoint_sign_product_factor + S (ff_p_lemma_endpoint_sign_product) = S ((S (ff_i_lemma_endpoint_sign_product)) * fc)) /\ exists ff_q_lemma_endpoint_sign_product_factor. fb = ff_q_lemma_endpoint_sign_product_factor * S ((S (ff_i_lemma_endpoint_sign_product)) * fc) + (ff_p_lemma_endpoint_sign_product))) /\ ((((exists ff_h_lemma_endpoint_sign_product_partial. ff_h_lemma_endpoint_sign_product_partial + S (ff_r_lemma_endpoint_sign_product) = S ((S (ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_partial. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_partial * S ((S (ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product) + (ff_r_lemma_endpoint_sign_product))) /\ ((((exists ff_h_lemma_endpoint_sign_product_successor. ff_h_lemma_endpoint_sign_product_successor + S (ff_s_lemma_endpoint_sign_product) = S ((S (S ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product)) /\ exists ff_q_lemma_endpoint_sign_product_successor. ff_u_lemma_endpoint_sign_product = ff_q_lemma_endpoint_sign_product_successor * S ((S (S ff_i_lemma_endpoint_sign_product)) * ff_v_lemma_endpoint_sign_product) + (ff_s_lemma_endpoint_sign_product))) /\ ff_s_lemma_endpoint_sign_product = ff_r_lemma_endpoint_sign_product * ff_p_lemma_endpoint_sign_product)))))) /\ ((exists ff_b_lemma_endpoint_sign_power_expanded ff_c_lemma_endpoint_sign_power_expanded. ((forall ff_i_lemma_endpoint_sign_power_expanded_repeat. (exists ff_lt_lemma_endpoint_sign_power_expanded_repeat_bound. ff_lt_lemma_endpoint_sign_power_expanded_repeat_bound + S ff_i_lemma_endpoint_sign_power_expanded_repeat = x4) -> (((exists ff_h_lemma_endpoint_sign_power_expanded_repeat_decoded. ff_h_lemma_endpoint_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_repeat_decoded. ff_b_lemma_endpoint_sign_power_expanded = ff_q_lemma_endpoint_sign_power_expanded_repeat_decoded * S ((S (ff_i_lemma_endpoint_sign_power_expanded_repeat)) * ff_c_lemma_endpoint_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_lemma_endpoint_sign_power_expanded_product ff_v_lemma_endpoint_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_start. ff_h_lemma_endpoint_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_start. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_start * S ((S (0)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_terminal. ff_h_lemma_endpoint_sign_power_expanded_product_terminal + S (R) = S ((S (x4)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_terminal. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_terminal * S ((S (x4)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (R))) /\ forall ff_i_lemma_endpoint_sign_power_expanded_product. (exists ff_lt_lemma_endpoint_sign_power_expanded_product_bound. ff_lt_lemma_endpoint_sign_power_expanded_product_bound + S ff_i_lemma_endpoint_sign_power_expanded_product = x4) -> exists ff_p_lemma_endpoint_sign_power_expanded_product ff_r_lemma_endpoint_sign_power_expanded_product ff_s_lemma_endpoint_sign_power_expanded_product. ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_factor. ff_h_lemma_endpoint_sign_power_expanded_product_factor + S (ff_p_lemma_endpoint_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_c_lemma_endpoint_sign_power_expanded)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_factor. ff_b_lemma_endpoint_sign_power_expanded = ff_q_lemma_endpoint_sign_power_expanded_product_factor * S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_c_lemma_endpoint_sign_power_expanded) + (ff_p_lemma_endpoint_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_partial. ff_h_lemma_endpoint_sign_power_expanded_product_partial + S (ff_r_lemma_endpoint_sign_power_expanded_product) = S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_partial. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_partial * S ((S (ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (ff_r_lemma_endpoint_sign_power_expanded_product))) /\ ((((exists ff_h_lemma_endpoint_sign_power_expanded_product_successor. ff_h_lemma_endpoint_sign_power_expanded_product_successor + S (ff_s_lemma_endpoint_sign_power_expanded_product) = S ((S (S ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product)) /\ exists ff_q_lemma_endpoint_sign_power_expanded_product_successor. ff_u_lemma_endpoint_sign_power_expanded_product = ff_q_lemma_endpoint_sign_power_expanded_product_successor * S ((S (S ff_i_lemma_endpoint_sign_power_expanded_product)) * ff_v_lemma_endpoint_sign_power_expanded_product) + (ff_s_lemma_endpoint_sign_power_expanded_product))) /\ ff_s_lemma_endpoint_sign_power_expanded_product = ff_r_lemma_endpoint_sign_power_expanded_product * ff_p_lemma_endpoint_sign_power_expanded_product)))))))) /\ Sprod = R)))
99. 0099specialize beta_sign_factor_product_power_exists p
100. 0100specialize beta_sign_factor_product_power_exists (2 * h)
101. 0101specialize beta_sign_factor_product_power_exists x2
102. 0102specialize beta_sign_factor_product_power_exists x3
103. 0103specialize beta_sign_factor_product_power_exists h
104. 0104specialize beta_sign_factor_product_power_exists x4
105. 0105apply beta_sign_factor_product_power_exists
106. 0106exact hpsucc
107. 0107exact hcount_exists_witness
108. 0108cases hsign_package
109. 0109cases hsign_package_witness
110. 0110cases hsign_package_witness_witness
111. 0111cases hsign_package_witness_witness_witness
112. 0112cases hsign_package_witness_witness_witness_witness
113. 0113cases hsign_package_witness_witness_witness_witness_right
114. 0114cases hsign_package_witness_witness_witness_witness_right_right
115. 0115have hpointwise_package : exists tb tc T. ((forall fpmp_index_lemma_endpoint_pointwise_products fpmp_left_lemma_endpoint_pointwise_products fpmp_right_lemma_endpoint_pointwise_products fpmp_target_lemma_endpoint_pointwise_products. (exists fpmp_gap_lemma_endpoint_pointwise_products. fpmp_gap_lemma_endpoint_pointwise_products + S fpmp_index_lemma_endpoint_pointwise_products = h) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_left. ff_h_fpmp_lemma_endpoint_pointwise_products_left + S (fpmp_left_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x1)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_left. x = ff_q_fpmp_lemma_endpoint_pointwise_products_left * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x1) + (fpmp_left_lemma_endpoint_pointwise_products))) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_right. ff_h_fpmp_lemma_endpoint_pointwise_products_right + S (fpmp_right_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x10)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_right. x9 = ff_q_fpmp_lemma_endpoint_pointwise_products_right * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * x10) + (fpmp_right_lemma_endpoint_pointwise_products))) -> (((exists ff_h_fpmp_lemma_endpoint_pointwise_products_target. ff_h_fpmp_lemma_endpoint_pointwise_products_target + S (fpmp_target_lemma_endpoint_pointwise_products) = S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * tc)) /\ exists ff_q_fpmp_lemma_endpoint_pointwise_products_target. tb = ff_q_fpmp_lemma_endpoint_pointwise_products_target * S ((S (fpmp_index_lemma_endpoint_pointwise_products)) * tc) + (fpmp_target_lemma_endpoint_pointwise_products))) -> fpmp_target_lemma_endpoint_pointwise_products = fpmp_left_lemma_endpoint_pointwise_products * fpmp_right_lemma_endpoint_pointwise_products) /\ ((exists ff_u_lemma_endpoint_target_product ff_v_lemma_endpoint_target_product. ((((exists ff_h_lemma_endpoint_target_product_start. ff_h_lemma_endpoint_target_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_start. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_start * S ((S (0)) * ff_v_lemma_endpoint_target_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_target_product_terminal. ff_h_lemma_endpoint_target_product_terminal + S (T) = S ((S (h)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_terminal. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_target_product) + (T))) /\ forall ff_i_lemma_endpoint_target_product. (exists ff_lt_lemma_endpoint_target_product_bound. ff_lt_lemma_endpoint_target_product_bound + S ff_i_lemma_endpoint_target_product = h) -> exists ff_p_lemma_endpoint_target_product ff_r_lemma_endpoint_target_product ff_s_lemma_endpoint_target_product. ((((exists ff_h_lemma_endpoint_target_product_factor. ff_h_lemma_endpoint_target_product_factor + S (ff_p_lemma_endpoint_target_product) = S ((S (ff_i_lemma_endpoint_target_product)) * tc)) /\ exists ff_q_lemma_endpoint_target_product_factor. tb = ff_q_lemma_endpoint_target_product_factor * S ((S (ff_i_lemma_endpoint_target_product)) * tc) + (ff_p_lemma_endpoint_target_product))) /\ ((((exists ff_h_lemma_endpoint_target_product_partial. ff_h_lemma_endpoint_target_product_partial + S (ff_r_lemma_endpoint_target_product) = S ((S (ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_partial. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_partial * S ((S (ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product) + (ff_r_lemma_endpoint_target_product))) /\ ((((exists ff_h_lemma_endpoint_target_product_successor. ff_h_lemma_endpoint_target_product_successor + S (ff_s_lemma_endpoint_target_product) = S ((S (S ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product)) /\ exists ff_q_lemma_endpoint_target_product_successor. ff_u_lemma_endpoint_target_product = ff_q_lemma_endpoint_target_product_successor * S ((S (S ff_i_lemma_endpoint_target_product)) * ff_v_lemma_endpoint_target_product) + (ff_s_lemma_endpoint_target_product))) /\ ff_s_lemma_endpoint_target_product = ff_r_lemma_endpoint_target_product * ff_p_lemma_endpoint_target_product)))))) /\ T = x8 * x11))
116. 0116specialize beta_pointwise_mul_product_exists x
117. 0117specialize beta_pointwise_mul_product_exists x1
118. 0118specialize beta_pointwise_mul_product_exists x9
119. 0119specialize beta_pointwise_mul_product_exists x10
120. 0120specialize beta_pointwise_mul_product_exists h
121. 0121specialize beta_pointwise_mul_product_exists x8
122. 0122specialize beta_pointwise_mul_product_exists x11
123. 0123apply beta_pointwise_mul_product_exists
124. 0124exact hmagnitude_product_exists_witness
125. 0125exact hsign_package_witness_witness_witness_witness_right_left
126. 0126cases hpointwise_package
127. 0127cases hpointwise_package_witness
128. 0128cases hpointwise_package_witness_witness
129. 0129cases hpointwise_package_witness_witness_witness
130. 0130cases hpointwise_package_witness_witness_witness_right
131. 0131have hmultiplier_power_exists : exists A. (exists ff_b_lemma_endpoint_multiplier_power ff_c_lemma_endpoint_multiplier_power. ((forall ff_i_lemma_endpoint_multiplier_power_repeat. (exists ff_lt_lemma_endpoint_multiplier_power_repeat_bound. ff_lt_lemma_endpoint_multiplier_power_repeat_bound + S ff_i_lemma_endpoint_multiplier_power_repeat = h) -> (((exists ff_h_lemma_endpoint_multiplier_power_repeat_decoded. ff_h_lemma_endpoint_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_repeat_decoded. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_repeat_decoded * S ((S (ff_i_lemma_endpoint_multiplier_power_repeat)) * ff_c_lemma_endpoint_multiplier_power) + (a)))) /\ (exists ff_u_lemma_endpoint_multiplier_power_product ff_v_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_start. ff_h_lemma_endpoint_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_start. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_start * S ((S (0)) * ff_v_lemma_endpoint_multiplier_power_product) + (1))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_terminal. ff_h_lemma_endpoint_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_terminal. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_terminal * S ((S (h)) * ff_v_lemma_endpoint_multiplier_power_product) + (A))) /\ forall ff_i_lemma_endpoint_multiplier_power_product. (exists ff_lt_lemma_endpoint_multiplier_power_product_bound. ff_lt_lemma_endpoint_multiplier_power_product_bound + S ff_i_lemma_endpoint_multiplier_power_product = h) -> exists ff_p_lemma_endpoint_multiplier_power_product ff_r_lemma_endpoint_multiplier_power_product ff_s_lemma_endpoint_multiplier_power_product. ((((exists ff_h_lemma_endpoint_multiplier_power_product_factor. ff_h_lemma_endpoint_multiplier_power_product_factor + S (ff_p_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_factor. ff_b_lemma_endpoint_multiplier_power = ff_q_lemma_endpoint_multiplier_power_product_factor * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_c_lemma_endpoint_multiplier_power) + (ff_p_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_partial. ff_h_lemma_endpoint_multiplier_power_product_partial + S (ff_r_lemma_endpoint_multiplier_power_product) = S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_partial. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_partial * S ((S (ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_r_lemma_endpoint_multiplier_power_product))) /\ ((((exists ff_h_lemma_endpoint_multiplier_power_product_successor. ff_h_lemma_endpoint_multiplier_power_product_successor + S (ff_s_lemma_endpoint_multiplier_power_product) = S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product)) /\ exists ff_q_lemma_endpoint_multiplier_power_product_successor. ff_u_lemma_endpoint_multiplier_power_product = ff_q_lemma_endpoint_multiplier_power_product_successor * S ((S (S ff_i_lemma_endpoint_multiplier_power_product)) * ff_v_lemma_endpoint_multiplier_power_product) + (ff_s_lemma_endpoint_multiplier_power_product))) /\ ff_s_lemma_endpoint_multiplier_power_product = ff_r_lemma_endpoint_multiplier_power_product * ff_p_lemma_endpoint_multiplier_power_product))))))))
132. 0132specialize pow_exists a
133. 0133specialize pow_exists h
134. 0134exact pow_exists
135. 0135cases hmultiplier_power_exists
136. 0136have hcancelled : exists gle_left_lemma_endpoint_local_result gle_right_lemma_endpoint_local_result. x16 + p * gle_left_lemma_endpoint_local_result = x12 + p * gle_right_lemma_endpoint_local_result
137. 0137specialize gauss_signed_products_cancel_mod p
138. 0138specialize gauss_signed_products_cancel_mod h
139. 0139specialize gauss_signed_products_cancel_mod (2 * h)
140. 0140specialize gauss_signed_products_cancel_mod a
141. 0141specialize gauss_signed_products_cancel_mod b
142. 0142specialize gauss_signed_products_cancel_mod c
143. 0143specialize gauss_signed_products_cancel_mod x
144. 0144specialize gauss_signed_products_cancel_mod x1
145. 0145specialize gauss_signed_products_cancel_mod x5
146. 0146specialize gauss_signed_products_cancel_mod x6
147. 0147specialize gauss_signed_products_cancel_mod x2
148. 0148specialize gauss_signed_products_cancel_mod x3
149. 0149specialize gauss_signed_products_cancel_mod x9
150. 0150specialize gauss_signed_products_cancel_mod x10
151. 0151specialize gauss_signed_products_cancel_mod x13
152. 0152specialize gauss_signed_products_cancel_mod x14
153. 0153specialize gauss_signed_products_cancel_mod x4
154. 0154specialize gauss_signed_products_cancel_mod x7
155. 0155specialize gauss_signed_products_cancel_mod x8
156. 0156specialize gauss_signed_products_cancel_mod x11
157. 0157specialize gauss_signed_products_cancel_mod x15
158. 0158specialize gauss_signed_products_cancel_mod x16
159. 0159specialize gauss_signed_products_cancel_mod x12
160. 0160apply gauss_signed_products_cancel_mod
161. 0161exact hprime
162. 0162exact hpsucc
163. 0163refl
164. 0164exact hsigned_exists_witness_witness_witness_witness
165. 0165exact hsign_package_witness_witness_witness_witness_left
166. 0166exact hpointwise_package_witness_witness_witness_left
167. 0167exact hmagnitude_range
168. 0168exact hmagnitude_injective
169. 0169exact hrecode_exists_witness_witness
170. 0170exact hhalf
171. 0171exact hcount_exists_witness
172. 0172exact hcanonical_product_exists_witness
173. 0173exact hmagnitude_product_exists_witness
174. 0174exact hsign_package_witness_witness_witness_witness_right_left
175. 0175exact hpointwise_package_witness_witness_witness_right_left
176. 0176exact hmultiplier_power_exists_witness
177. 0177exact hsign_package_witness_witness_witness_witness_right_right_left
178. 0178exists x4
179. 0179exists x16
180. 0180exists x12
181. 0181split
182. 0182exact hmultiplier_power_exists_witness
183. 0183split
184. 0184exact hsign_package_witness_witness_witness_witness_right_right_left
185. 0185split
186. 0186exists x
187. 0187exists x1
188. 0188exists x2
189. 0189exists x3
190. 0190split
191. 0191exact hsigned_exists_witness_witness_witness_witness
192. 0192exact hcount_exists_witness
193. 0193exact hcancelled