distinct_odd_primes_gauss_eisenstein_data_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 q
3. 0003intro h
4. 0004intro k
5. 0005intro hpodd
6. 0006intro hqodd
7. 0007intro hp
8. 0008intro hq
9. 0009intro hpq
10. 0010have hmutual : ((~(exists gsp_divisor_factor_ged_pair_p_not_q. q = p * gsp_divisor_factor_ged_pair_p_not_q)) /\ (~(exists gsp_divisor_factor_ged_pair_q_not_p. p = q * gsp_divisor_factor_ged_pair_q_not_p)))
11. 0011specialize distinct_primes_mutually_nondivisible p
12. 0012specialize distinct_primes_mutually_nondivisible q
13. 0013apply distinct_primes_mutually_nondivisible
14. 0014exact hp
15. 0015exact hq
16. 0016exact hpq
17. 0017cases hmutual
18. 0018have hq_odd : exists gs_odd_ged_pair_q_odd. q = 2 * gs_odd_ged_pair_q_odd + 1
19. 0019exists k
20. 0020exact hqodd
21. 0021have hp_odd : exists gs_odd_ged_pair_p_odd. p = 2 * gs_odd_ged_pair_p_odd + 1
22. 0022exists h
23. 0023exact hpodd
24. 0024have hfirst : exists tb tc qb qc rb rc e Q. ((forall esd_index_ged_pair_first_scaled esd_value_ged_pair_first_scaled. (exists esd_gap_ged_pair_first_scaled. esd_gap_ged_pair_first_scaled + S esd_index_ged_pair_first_scaled = h) -> (((exists ff_h_esd_ged_pair_first_scaled_decoded. ff_h_esd_ged_pair_first_scaled_decoded + S (esd_value_ged_pair_first_scaled) = S ((S (esd_index_ged_pair_first_scaled)) * tc)) /\ exists ff_q_esd_ged_pair_first_scaled_decoded. tb = ff_q_esd_ged_pair_first_scaled_decoded * S ((S (esd_index_ged_pair_first_scaled)) * tc) + (esd_value_ged_pair_first_scaled))) -> esd_value_ged_pair_first_scaled = q * (1 + esd_index_ged_pair_first_scaled)) /\ ((forall fdp_index_ged_pair_first_division. (exists gsp_lt_gap_ged_pair_first_division_index_bound. gsp_lt_gap_ged_pair_first_division_index_bound + S fdp_index_ged_pair_first_division = h) -> exists fdp_value_ged_pair_first_division fdp_quotient_ged_pair_first_division fdp_remainder_ged_pair_first_division. (((exists ff_h_fdp_ged_pair_first_division_source. ff_h_fdp_ged_pair_first_division_source + S (fdp_value_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * tc)) /\ exists ff_q_fdp_ged_pair_first_division_source. tb = ff_q_fdp_ged_pair_first_division_source * S ((S (fdp_index_ged_pair_first_division)) * tc) + (fdp_value_ged_pair_first_division))) /\ ((((exists ff_h_fdp_ged_pair_first_division_quotient_entry. ff_h_fdp_ged_pair_first_division_quotient_entry + S (fdp_quotient_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * qc)) /\ exists ff_q_fdp_ged_pair_first_division_quotient_entry. qb = ff_q_fdp_ged_pair_first_division_quotient_entry * S ((S (fdp_index_ged_pair_first_division)) * qc) + (fdp_quotient_ged_pair_first_division))) /\ ((((exists ff_h_fdp_ged_pair_first_division_remainder_entry. ff_h_fdp_ged_pair_first_division_remainder_entry + S (fdp_remainder_ged_pair_first_division) = S ((S (fdp_index_ged_pair_first_division)) * rc)) /\ exists ff_q_fdp_ged_pair_first_division_remainder_entry. rb = ff_q_fdp_ged_pair_first_division_remainder_entry * S ((S (fdp_index_ged_pair_first_division)) * rc) + (fdp_remainder_ged_pair_first_division))) /\ (fdp_value_ged_pair_first_division = p * fdp_quotient_ged_pair_first_division + fdp_remainder_ged_pair_first_division /\ (exists gsp_lt_gap_ged_pair_first_division_remainder_bound. gsp_lt_gap_ged_pair_first_division_remainder_bound + S fdp_remainder_ged_pair_first_division = p))))) /\ ((exists ff_u_ged_pair_first_sum ff_v_ged_pair_first_sum. ((((exists ff_h_ged_pair_first_sum_start. ff_h_ged_pair_first_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_start. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_start * S ((S (0)) * ff_v_ged_pair_first_sum) + (0))) /\ ((((exists ff_h_ged_pair_first_sum_terminal. ff_h_ged_pair_first_sum_terminal + S (Q) = S ((S (h)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_terminal. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_terminal * S ((S (h)) * ff_v_ged_pair_first_sum) + (Q))) /\ forall ff_i_ged_pair_first_sum. (exists ff_lt_ged_pair_first_sum_bound. ff_lt_ged_pair_first_sum_bound + S ff_i_ged_pair_first_sum = h) -> exists ff_a_ged_pair_first_sum ff_r_ged_pair_first_sum ff_s_ged_pair_first_sum. ((((exists ff_h_ged_pair_first_sum_summand. ff_h_ged_pair_first_sum_summand + S (ff_a_ged_pair_first_sum) = S ((S (ff_i_ged_pair_first_sum)) * qc)) /\ exists ff_q_ged_pair_first_sum_summand. qb = ff_q_ged_pair_first_sum_summand * S ((S (ff_i_ged_pair_first_sum)) * qc) + (ff_a_ged_pair_first_sum))) /\ ((((exists ff_h_ged_pair_first_sum_partial. ff_h_ged_pair_first_sum_partial + S (ff_r_ged_pair_first_sum) = S ((S (ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_partial. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_partial * S ((S (ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum) + (ff_r_ged_pair_first_sum))) /\ ((((exists ff_h_ged_pair_first_sum_successor. ff_h_ged_pair_first_sum_successor + S (ff_s_ged_pair_first_sum) = S ((S (S ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum)) /\ exists ff_q_ged_pair_first_sum_successor. ff_u_ged_pair_first_sum = ff_q_ged_pair_first_sum_successor * S ((S (S ff_i_ged_pair_first_sum)) * ff_v_ged_pair_first_sum) + (ff_s_ged_pair_first_sum))) /\ ff_s_ged_pair_first_sum = ff_r_ged_pair_first_sum + ff_a_ged_pair_first_sum)))))) /\ (((((((exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres) -> (exists gs_even_ged_pair_first_hidden_classification_even. e = 2 * gs_even_ged_pair_first_hidden_classification_even)) /\ ((exists gs_even_ged_pair_first_hidden_classification_even. e = 2 * gs_even_ged_pair_first_hidden_classification_even) -> (exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres)))) /\ (((~(exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres) -> (exists gs_odd_ged_pair_first_hidden_classification_odd. e = 2 * gs_odd_ged_pair_first_hidden_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_first_hidden_classification_odd. e = 2 * gs_odd_ged_pair_first_hidden_classification_odd + 1) -> ~(exists qr_x_ged_pair_first_hidden_classification_qres. exists qr_u_ged_pair_first_hidden_classification_qres qr_v_ged_pair_first_hidden_classification_qres. qr_x_ged_pair_first_hidden_classification_qres * qr_x_ged_pair_first_hidden_classification_qres + p * qr_u_ged_pair_first_hidden_classification_qres = q + p * qr_v_ged_pair_first_hidden_classification_qres)))))) /\ (exists fspm_u_ged_pair_first_hidden_mod fspm_v_ged_pair_first_hidden_mod. (e) + 2 * fspm_u_ged_pair_first_hidden_mod = (Q) + 2 * fspm_v_ged_pair_first_hidden_mod)))))
25. 0025specialize odd_prime_gauss_eisenstein_orientation_data_exists p
26. 0026specialize odd_prime_gauss_eisenstein_orientation_data_exists h
27. 0027specialize odd_prime_gauss_eisenstein_orientation_data_exists q
28. 0028apply odd_prime_gauss_eisenstein_orientation_data_exists
29. 0029exact hpodd
30. 0030exact hq_odd
31. 0031exact hp
32. 0032exact hmutual_left
33. 0033cases hfirst
34. 0034cases hfirst_witness
35. 0035cases hfirst_witness_witness
36. 0036cases hfirst_witness_witness_witness
37. 0037cases hfirst_witness_witness_witness_witness
38. 0038cases hfirst_witness_witness_witness_witness_witness
39. 0039cases hfirst_witness_witness_witness_witness_witness_witness
40. 0040cases hfirst_witness_witness_witness_witness_witness_witness_witness
41. 0041cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness
42. 0042cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right
43. 0043cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right
44. 0044cases hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
45. 0045have hsecond : exists tb tc qb qc rb rc e Q. ((forall esd_index_ged_pair_second_scaled esd_value_ged_pair_second_scaled. (exists esd_gap_ged_pair_second_scaled. esd_gap_ged_pair_second_scaled + S esd_index_ged_pair_second_scaled = k) -> (((exists ff_h_esd_ged_pair_second_scaled_decoded. ff_h_esd_ged_pair_second_scaled_decoded + S (esd_value_ged_pair_second_scaled) = S ((S (esd_index_ged_pair_second_scaled)) * tc)) /\ exists ff_q_esd_ged_pair_second_scaled_decoded. tb = ff_q_esd_ged_pair_second_scaled_decoded * S ((S (esd_index_ged_pair_second_scaled)) * tc) + (esd_value_ged_pair_second_scaled))) -> esd_value_ged_pair_second_scaled = p * (1 + esd_index_ged_pair_second_scaled)) /\ ((forall fdp_index_ged_pair_second_division. (exists gsp_lt_gap_ged_pair_second_division_index_bound. gsp_lt_gap_ged_pair_second_division_index_bound + S fdp_index_ged_pair_second_division = k) -> exists fdp_value_ged_pair_second_division fdp_quotient_ged_pair_second_division fdp_remainder_ged_pair_second_division. (((exists ff_h_fdp_ged_pair_second_division_source. ff_h_fdp_ged_pair_second_division_source + S (fdp_value_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * tc)) /\ exists ff_q_fdp_ged_pair_second_division_source. tb = ff_q_fdp_ged_pair_second_division_source * S ((S (fdp_index_ged_pair_second_division)) * tc) + (fdp_value_ged_pair_second_division))) /\ ((((exists ff_h_fdp_ged_pair_second_division_quotient_entry. ff_h_fdp_ged_pair_second_division_quotient_entry + S (fdp_quotient_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * qc)) /\ exists ff_q_fdp_ged_pair_second_division_quotient_entry. qb = ff_q_fdp_ged_pair_second_division_quotient_entry * S ((S (fdp_index_ged_pair_second_division)) * qc) + (fdp_quotient_ged_pair_second_division))) /\ ((((exists ff_h_fdp_ged_pair_second_division_remainder_entry. ff_h_fdp_ged_pair_second_division_remainder_entry + S (fdp_remainder_ged_pair_second_division) = S ((S (fdp_index_ged_pair_second_division)) * rc)) /\ exists ff_q_fdp_ged_pair_second_division_remainder_entry. rb = ff_q_fdp_ged_pair_second_division_remainder_entry * S ((S (fdp_index_ged_pair_second_division)) * rc) + (fdp_remainder_ged_pair_second_division))) /\ (fdp_value_ged_pair_second_division = q * fdp_quotient_ged_pair_second_division + fdp_remainder_ged_pair_second_division /\ (exists gsp_lt_gap_ged_pair_second_division_remainder_bound. gsp_lt_gap_ged_pair_second_division_remainder_bound + S fdp_remainder_ged_pair_second_division = q))))) /\ ((exists ff_u_ged_pair_second_sum ff_v_ged_pair_second_sum. ((((exists ff_h_ged_pair_second_sum_start. ff_h_ged_pair_second_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_start. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_start * S ((S (0)) * ff_v_ged_pair_second_sum) + (0))) /\ ((((exists ff_h_ged_pair_second_sum_terminal. ff_h_ged_pair_second_sum_terminal + S (Q) = S ((S (k)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_terminal. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_terminal * S ((S (k)) * ff_v_ged_pair_second_sum) + (Q))) /\ forall ff_i_ged_pair_second_sum. (exists ff_lt_ged_pair_second_sum_bound. ff_lt_ged_pair_second_sum_bound + S ff_i_ged_pair_second_sum = k) -> exists ff_a_ged_pair_second_sum ff_r_ged_pair_second_sum ff_s_ged_pair_second_sum. ((((exists ff_h_ged_pair_second_sum_summand. ff_h_ged_pair_second_sum_summand + S (ff_a_ged_pair_second_sum) = S ((S (ff_i_ged_pair_second_sum)) * qc)) /\ exists ff_q_ged_pair_second_sum_summand. qb = ff_q_ged_pair_second_sum_summand * S ((S (ff_i_ged_pair_second_sum)) * qc) + (ff_a_ged_pair_second_sum))) /\ ((((exists ff_h_ged_pair_second_sum_partial. ff_h_ged_pair_second_sum_partial + S (ff_r_ged_pair_second_sum) = S ((S (ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_partial. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_partial * S ((S (ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum) + (ff_r_ged_pair_second_sum))) /\ ((((exists ff_h_ged_pair_second_sum_successor. ff_h_ged_pair_second_sum_successor + S (ff_s_ged_pair_second_sum) = S ((S (S ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum)) /\ exists ff_q_ged_pair_second_sum_successor. ff_u_ged_pair_second_sum = ff_q_ged_pair_second_sum_successor * S ((S (S ff_i_ged_pair_second_sum)) * ff_v_ged_pair_second_sum) + (ff_s_ged_pair_second_sum))) /\ ff_s_ged_pair_second_sum = ff_r_ged_pair_second_sum + ff_a_ged_pair_second_sum)))))) /\ (((((((exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres) -> (exists gs_even_ged_pair_second_hidden_classification_even. e = 2 * gs_even_ged_pair_second_hidden_classification_even)) /\ ((exists gs_even_ged_pair_second_hidden_classification_even. e = 2 * gs_even_ged_pair_second_hidden_classification_even) -> (exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres)))) /\ (((~(exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres) -> (exists gs_odd_ged_pair_second_hidden_classification_odd. e = 2 * gs_odd_ged_pair_second_hidden_classification_odd + 1)) /\ ((exists gs_odd_ged_pair_second_hidden_classification_odd. e = 2 * gs_odd_ged_pair_second_hidden_classification_odd + 1) -> ~(exists qr_x_ged_pair_second_hidden_classification_qres. exists qr_u_ged_pair_second_hidden_classification_qres qr_v_ged_pair_second_hidden_classification_qres. qr_x_ged_pair_second_hidden_classification_qres * qr_x_ged_pair_second_hidden_classification_qres + q * qr_u_ged_pair_second_hidden_classification_qres = p + q * qr_v_ged_pair_second_hidden_classification_qres)))))) /\ (exists fspm_u_ged_pair_second_hidden_mod fspm_v_ged_pair_second_hidden_mod. (e) + 2 * fspm_u_ged_pair_second_hidden_mod = (Q) + 2 * fspm_v_ged_pair_second_hidden_mod)))))
46. 0046specialize odd_prime_gauss_eisenstein_orientation_data_exists q
47. 0047specialize odd_prime_gauss_eisenstein_orientation_data_exists k
48. 0048specialize odd_prime_gauss_eisenstein_orientation_data_exists p
49. 0049apply odd_prime_gauss_eisenstein_orientation_data_exists
50. 0050exact hqodd
51. 0051exact hp_odd
52. 0052exact hq
53. 0053exact hmutual_right
54. 0054cases hsecond
55. 0055cases hsecond_witness
56. 0056cases hsecond_witness_witness
57. 0057cases hsecond_witness_witness_witness
58. 0058cases hsecond_witness_witness_witness_witness
59. 0059cases hsecond_witness_witness_witness_witness_witness
60. 0060cases hsecond_witness_witness_witness_witness_witness_witness
61. 0061cases hsecond_witness_witness_witness_witness_witness_witness_witness
62. 0062cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness
63. 0063cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right
64. 0064cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right
65. 0065cases hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right
66. 0066have hqp : ~(q = p)
67. 0067intro hqp_eq
68. 0068apply hpq
69. 0069symm
70. 0070exact hqp_eq
71. 0071have hfirst_rectangle : exists cb cc total. ((forall erc_row_ged_pair_first_rectangle. (exists erc_lt_gap_ged_pair_first_rectangle_bound. erc_lt_gap_ged_pair_first_rectangle_bound + S (erc_row_ged_pair_first_rectangle) = h) -> exists erc_count_ged_pair_first_rectangle. ((((exists ff_h_erc_ged_pair_first_rectangle_decoded. ff_h_erc_ged_pair_first_rectangle_decoded + S (erc_count_ged_pair_first_rectangle) = S ((S (erc_row_ged_pair_first_rectangle)) * cc)) /\ exists ff_q_erc_ged_pair_first_rectangle_decoded. cb = ff_q_erc_ged_pair_first_rectangle_decoded * S ((S (erc_row_ged_pair_first_rectangle)) * cc) + (erc_count_ged_pair_first_rectangle))) /\ (exists erc_row_code_ged_pair_first_rectangle_witness erc_row_scale_ged_pair_first_rectangle_witness. ((forall eri_column_erc_ged_pair_first_rectangle_witness_row. (exists eri_gap_erc_ged_pair_first_rectangle_witness_row_bound. eri_gap_erc_ged_pair_first_rectangle_witness_row_bound + S (eri_column_erc_ged_pair_first_rectangle_witness_row) = k) -> exists eri_bit_erc_ged_pair_first_rectangle_witness_row. ((((exists ff_h_eri_erc_ged_pair_first_rectangle_witness_row_decoded. ff_h_eri_erc_ged_pair_first_rectangle_witness_row_decoded + S (eri_bit_erc_ged_pair_first_rectangle_witness_row) = S ((S (eri_column_erc_ged_pair_first_rectangle_witness_row)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_eri_erc_ged_pair_first_rectangle_witness_row_decoded. erc_row_code_ged_pair_first_rectangle_witness = ff_q_eri_erc_ged_pair_first_rectangle_witness_row_decoded * S ((S (eri_column_erc_ged_pair_first_rectangle_witness_row)) * erc_row_scale_ged_pair_first_rectangle_witness) + (eri_bit_erc_ged_pair_first_rectangle_witness_row))) /\ (((eri_bit_erc_ged_pair_first_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left + S (q * S erc_row_ged_pair_first_rectangle) = p * S eri_column_erc_ged_pair_first_rectangle_witness_row) /\ ~(exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right + S (p * S eri_column_erc_ged_pair_first_rectangle_witness_row) = q * S erc_row_ged_pair_first_rectangle))) \/ (eri_bit_erc_ged_pair_first_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_right + S (p * S eri_column_erc_ged_pair_first_rectangle_witness_row) = q * S erc_row_ged_pair_first_rectangle) /\ ~(exists eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_first_rectangle_witness_row_choice_left + S (q * S erc_row_ged_pair_first_rectangle) = p * S eri_column_erc_ged_pair_first_rectangle_witness_row))))))) /\ (((exists ff_u_erc_ged_pair_first_rectangle_witness_count_sum ff_v_erc_ged_pair_first_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_start. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_start. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_terminal. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_terminal + S (erc_count_ged_pair_first_rectangle) = S ((S (k)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_terminal. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_terminal * S ((S (k)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (erc_count_ged_pair_first_rectangle))) /\ forall ff_i_erc_ged_pair_first_rectangle_witness_count_sum. (exists ff_lt_erc_ged_pair_first_rectangle_witness_count_sum_bound. ff_lt_erc_ged_pair_first_rectangle_witness_count_sum_bound + S ff_i_erc_ged_pair_first_rectangle_witness_count_sum = k) -> exists ff_a_erc_ged_pair_first_rectangle_witness_count_sum ff_r_erc_ged_pair_first_rectangle_witness_count_sum ff_s_erc_ged_pair_first_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_summand. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_summand + S (ff_a_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_summand. erc_row_code_ged_pair_first_rectangle_witness = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_first_rectangle_witness) + (ff_a_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_partial. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_partial + S (ff_r_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_partial. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (ff_r_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_sum_successor. ff_h_erc_ged_pair_first_rectangle_witness_count_sum_successor + S (ff_s_erc_ged_pair_first_rectangle_witness_count_sum) = S ((S (S ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_sum_successor. ff_u_erc_ged_pair_first_rectangle_witness_count_sum = ff_q_erc_ged_pair_first_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_ged_pair_first_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_first_rectangle_witness_count_sum) + (ff_s_erc_ged_pair_first_rectangle_witness_count_sum))) /\ ff_s_erc_ged_pair_first_rectangle_witness_count_sum = ff_r_erc_ged_pair_first_rectangle_witness_count_sum + ff_a_erc_ged_pair_first_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_ged_pair_first_rectangle_witness_count_bits. (exists ff_lt_erc_ged_pair_first_rectangle_witness_count_bits_bound. ff_lt_erc_ged_pair_first_rectangle_witness_count_bits_bound + S ff_i_erc_ged_pair_first_rectangle_witness_count_bits = k) -> exists ff_bit_erc_ged_pair_first_rectangle_witness_count_bits. ((((exists ff_h_erc_ged_pair_first_rectangle_witness_count_bits_decoded. ff_h_erc_ged_pair_first_rectangle_witness_count_bits_decoded + S (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits) = S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_first_rectangle_witness)) /\ exists ff_q_erc_ged_pair_first_rectangle_witness_count_bits_decoded. erc_row_code_ged_pair_first_rectangle_witness = ff_q_erc_ged_pair_first_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_ged_pair_first_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_first_rectangle_witness) + (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits))) /\ (ff_bit_erc_ged_pair_first_rectangle_witness_count_bits = 0 \/ ff_bit_erc_ged_pair_first_rectangle_witness_count_bits = 1))))))))) /\ (exists ff_u_ged_pair_first_rectangle_sum ff_v_ged_pair_first_rectangle_sum. ((((exists ff_h_ged_pair_first_rectangle_sum_start. ff_h_ged_pair_first_rectangle_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_start. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_start * S ((S (0)) * ff_v_ged_pair_first_rectangle_sum) + (0))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_terminal. ff_h_ged_pair_first_rectangle_sum_terminal + S (total) = S ((S (h)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_terminal. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_terminal * S ((S (h)) * ff_v_ged_pair_first_rectangle_sum) + (total))) /\ forall ff_i_ged_pair_first_rectangle_sum. (exists ff_lt_ged_pair_first_rectangle_sum_bound. ff_lt_ged_pair_first_rectangle_sum_bound + S ff_i_ged_pair_first_rectangle_sum = h) -> exists ff_a_ged_pair_first_rectangle_sum ff_r_ged_pair_first_rectangle_sum ff_s_ged_pair_first_rectangle_sum. ((((exists ff_h_ged_pair_first_rectangle_sum_summand. ff_h_ged_pair_first_rectangle_sum_summand + S (ff_a_ged_pair_first_rectangle_sum) = S ((S (ff_i_ged_pair_first_rectangle_sum)) * cc)) /\ exists ff_q_ged_pair_first_rectangle_sum_summand. cb = ff_q_ged_pair_first_rectangle_sum_summand * S ((S (ff_i_ged_pair_first_rectangle_sum)) * cc) + (ff_a_ged_pair_first_rectangle_sum))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_partial. ff_h_ged_pair_first_rectangle_sum_partial + S (ff_r_ged_pair_first_rectangle_sum) = S ((S (ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_partial. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_partial * S ((S (ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum) + (ff_r_ged_pair_first_rectangle_sum))) /\ ((((exists ff_h_ged_pair_first_rectangle_sum_successor. ff_h_ged_pair_first_rectangle_sum_successor + S (ff_s_ged_pair_first_rectangle_sum) = S ((S (S ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum)) /\ exists ff_q_ged_pair_first_rectangle_sum_successor. ff_u_ged_pair_first_rectangle_sum = ff_q_ged_pair_first_rectangle_sum_successor * S ((S (S ff_i_ged_pair_first_rectangle_sum)) * ff_v_ged_pair_first_rectangle_sum) + (ff_s_ged_pair_first_rectangle_sum))) /\ ff_s_ged_pair_first_rectangle_sum = ff_r_ged_pair_first_rectangle_sum + ff_a_ged_pair_first_rectangle_sum)))))))
72. 0072specialize distinct_odd_prime_half_rectangle_total_exists p
73. 0073specialize distinct_odd_prime_half_rectangle_total_exists q
74. 0074specialize distinct_odd_prime_half_rectangle_total_exists h
75. 0075specialize distinct_odd_prime_half_rectangle_total_exists k
76. 0076apply distinct_odd_prime_half_rectangle_total_exists
77. 0077exact hpodd
78. 0078exact hqodd
79. 0079exact hp
80. 0080exact hq
81. 0081exact hpq
82. 0082cases hfirst_rectangle
83. 0083cases hfirst_rectangle_witness
84. 0084cases hfirst_rectangle_witness_witness
85. 0085cases hfirst_rectangle_witness_witness_witness
86. 0086have hsecond_rectangle : exists cb cc total. ((forall erc_row_ged_pair_second_rectangle. (exists erc_lt_gap_ged_pair_second_rectangle_bound. erc_lt_gap_ged_pair_second_rectangle_bound + S (erc_row_ged_pair_second_rectangle) = k) -> exists erc_count_ged_pair_second_rectangle. ((((exists ff_h_erc_ged_pair_second_rectangle_decoded. ff_h_erc_ged_pair_second_rectangle_decoded + S (erc_count_ged_pair_second_rectangle) = S ((S (erc_row_ged_pair_second_rectangle)) * cc)) /\ exists ff_q_erc_ged_pair_second_rectangle_decoded. cb = ff_q_erc_ged_pair_second_rectangle_decoded * S ((S (erc_row_ged_pair_second_rectangle)) * cc) + (erc_count_ged_pair_second_rectangle))) /\ (exists erc_row_code_ged_pair_second_rectangle_witness erc_row_scale_ged_pair_second_rectangle_witness. ((forall eri_column_erc_ged_pair_second_rectangle_witness_row. (exists eri_gap_erc_ged_pair_second_rectangle_witness_row_bound. eri_gap_erc_ged_pair_second_rectangle_witness_row_bound + S (eri_column_erc_ged_pair_second_rectangle_witness_row) = h) -> exists eri_bit_erc_ged_pair_second_rectangle_witness_row. ((((exists ff_h_eri_erc_ged_pair_second_rectangle_witness_row_decoded. ff_h_eri_erc_ged_pair_second_rectangle_witness_row_decoded + S (eri_bit_erc_ged_pair_second_rectangle_witness_row) = S ((S (eri_column_erc_ged_pair_second_rectangle_witness_row)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_eri_erc_ged_pair_second_rectangle_witness_row_decoded. erc_row_code_ged_pair_second_rectangle_witness = ff_q_eri_erc_ged_pair_second_rectangle_witness_row_decoded * S ((S (eri_column_erc_ged_pair_second_rectangle_witness_row)) * erc_row_scale_ged_pair_second_rectangle_witness) + (eri_bit_erc_ged_pair_second_rectangle_witness_row))) /\ (((eri_bit_erc_ged_pair_second_rectangle_witness_row = 0 /\ ((exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left + S (p * S erc_row_ged_pair_second_rectangle) = q * S eri_column_erc_ged_pair_second_rectangle_witness_row) /\ ~(exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right + S (q * S eri_column_erc_ged_pair_second_rectangle_witness_row) = p * S erc_row_ged_pair_second_rectangle))) \/ (eri_bit_erc_ged_pair_second_rectangle_witness_row = 1 /\ ((exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_right + S (q * S eri_column_erc_ged_pair_second_rectangle_witness_row) = p * S erc_row_ged_pair_second_rectangle) /\ ~(exists eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left. eri_gap_erc_ged_pair_second_rectangle_witness_row_choice_left + S (p * S erc_row_ged_pair_second_rectangle) = q * S eri_column_erc_ged_pair_second_rectangle_witness_row))))))) /\ (((exists ff_u_erc_ged_pair_second_rectangle_witness_count_sum ff_v_erc_ged_pair_second_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_start. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_start + S (0) = S ((S (0)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_start. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_start * S ((S (0)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (0))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_terminal. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_terminal + S (erc_count_ged_pair_second_rectangle) = S ((S (h)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_terminal. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_terminal * S ((S (h)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (erc_count_ged_pair_second_rectangle))) /\ forall ff_i_erc_ged_pair_second_rectangle_witness_count_sum. (exists ff_lt_erc_ged_pair_second_rectangle_witness_count_sum_bound. ff_lt_erc_ged_pair_second_rectangle_witness_count_sum_bound + S ff_i_erc_ged_pair_second_rectangle_witness_count_sum = h) -> exists ff_a_erc_ged_pair_second_rectangle_witness_count_sum ff_r_erc_ged_pair_second_rectangle_witness_count_sum ff_s_erc_ged_pair_second_rectangle_witness_count_sum. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_summand. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_summand + S (ff_a_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_summand. erc_row_code_ged_pair_second_rectangle_witness = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_summand * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * erc_row_scale_ged_pair_second_rectangle_witness) + (ff_a_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_partial. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_partial + S (ff_r_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_partial. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_partial * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (ff_r_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_sum_successor. ff_h_erc_ged_pair_second_rectangle_witness_count_sum_successor + S (ff_s_erc_ged_pair_second_rectangle_witness_count_sum) = S ((S (S ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_sum_successor. ff_u_erc_ged_pair_second_rectangle_witness_count_sum = ff_q_erc_ged_pair_second_rectangle_witness_count_sum_successor * S ((S (S ff_i_erc_ged_pair_second_rectangle_witness_count_sum)) * ff_v_erc_ged_pair_second_rectangle_witness_count_sum) + (ff_s_erc_ged_pair_second_rectangle_witness_count_sum))) /\ ff_s_erc_ged_pair_second_rectangle_witness_count_sum = ff_r_erc_ged_pair_second_rectangle_witness_count_sum + ff_a_erc_ged_pair_second_rectangle_witness_count_sum)))))) /\ (forall ff_i_erc_ged_pair_second_rectangle_witness_count_bits. (exists ff_lt_erc_ged_pair_second_rectangle_witness_count_bits_bound. ff_lt_erc_ged_pair_second_rectangle_witness_count_bits_bound + S ff_i_erc_ged_pair_second_rectangle_witness_count_bits = h) -> exists ff_bit_erc_ged_pair_second_rectangle_witness_count_bits. ((((exists ff_h_erc_ged_pair_second_rectangle_witness_count_bits_decoded. ff_h_erc_ged_pair_second_rectangle_witness_count_bits_decoded + S (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits) = S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_second_rectangle_witness)) /\ exists ff_q_erc_ged_pair_second_rectangle_witness_count_bits_decoded. erc_row_code_ged_pair_second_rectangle_witness = ff_q_erc_ged_pair_second_rectangle_witness_count_bits_decoded * S ((S (ff_i_erc_ged_pair_second_rectangle_witness_count_bits)) * erc_row_scale_ged_pair_second_rectangle_witness) + (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits))) /\ (ff_bit_erc_ged_pair_second_rectangle_witness_count_bits = 0 \/ ff_bit_erc_ged_pair_second_rectangle_witness_count_bits = 1))))))))) /\ (exists ff_u_ged_pair_second_rectangle_sum ff_v_ged_pair_second_rectangle_sum. ((((exists ff_h_ged_pair_second_rectangle_sum_start. ff_h_ged_pair_second_rectangle_sum_start + S (0) = S ((S (0)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_start. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_start * S ((S (0)) * ff_v_ged_pair_second_rectangle_sum) + (0))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_terminal. ff_h_ged_pair_second_rectangle_sum_terminal + S (total) = S ((S (k)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_terminal. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_terminal * S ((S (k)) * ff_v_ged_pair_second_rectangle_sum) + (total))) /\ forall ff_i_ged_pair_second_rectangle_sum. (exists ff_lt_ged_pair_second_rectangle_sum_bound. ff_lt_ged_pair_second_rectangle_sum_bound + S ff_i_ged_pair_second_rectangle_sum = k) -> exists ff_a_ged_pair_second_rectangle_sum ff_r_ged_pair_second_rectangle_sum ff_s_ged_pair_second_rectangle_sum. ((((exists ff_h_ged_pair_second_rectangle_sum_summand. ff_h_ged_pair_second_rectangle_sum_summand + S (ff_a_ged_pair_second_rectangle_sum) = S ((S (ff_i_ged_pair_second_rectangle_sum)) * cc)) /\ exists ff_q_ged_pair_second_rectangle_sum_summand. cb = ff_q_ged_pair_second_rectangle_sum_summand * S ((S (ff_i_ged_pair_second_rectangle_sum)) * cc) + (ff_a_ged_pair_second_rectangle_sum))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_partial. ff_h_ged_pair_second_rectangle_sum_partial + S (ff_r_ged_pair_second_rectangle_sum) = S ((S (ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_partial. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_partial * S ((S (ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum) + (ff_r_ged_pair_second_rectangle_sum))) /\ ((((exists ff_h_ged_pair_second_rectangle_sum_successor. ff_h_ged_pair_second_rectangle_sum_successor + S (ff_s_ged_pair_second_rectangle_sum) = S ((S (S ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum)) /\ exists ff_q_ged_pair_second_rectangle_sum_successor. ff_u_ged_pair_second_rectangle_sum = ff_q_ged_pair_second_rectangle_sum_successor * S ((S (S ff_i_ged_pair_second_rectangle_sum)) * ff_v_ged_pair_second_rectangle_sum) + (ff_s_ged_pair_second_rectangle_sum))) /\ ff_s_ged_pair_second_rectangle_sum = ff_r_ged_pair_second_rectangle_sum + ff_a_ged_pair_second_rectangle_sum)))))))
87. 0087specialize distinct_odd_prime_half_rectangle_total_exists q
88. 0088specialize distinct_odd_prime_half_rectangle_total_exists p
89. 0089specialize distinct_odd_prime_half_rectangle_total_exists k
90. 0090specialize distinct_odd_prime_half_rectangle_total_exists h
91. 0091apply distinct_odd_prime_half_rectangle_total_exists
92. 0092exact hqodd
93. 0093exact hpodd
94. 0094exact hq
95. 0095exact hp
96. 0096exact hqp
97. 0097cases hsecond_rectangle
98. 0098cases hsecond_rectangle_witness
99. 0099cases hsecond_rectangle_witness_witness
100. 0100cases hsecond_rectangle_witness_witness_witness
101. 0101have hsum_identity : x7 + x15 = h * k
102. 0102specialize distinct_odd_prime_eisenstein_quotient_sum_identity p
103. 0103specialize distinct_odd_prime_eisenstein_quotient_sum_identity q
104. 0104specialize distinct_odd_prime_eisenstein_quotient_sum_identity h
105. 0105specialize distinct_odd_prime_eisenstein_quotient_sum_identity k
106. 0106specialize distinct_odd_prime_eisenstein_quotient_sum_identity x
107. 0107specialize distinct_odd_prime_eisenstein_quotient_sum_identity x1
108. 0108specialize distinct_odd_prime_eisenstein_quotient_sum_identity x2
109. 0109specialize distinct_odd_prime_eisenstein_quotient_sum_identity x3
110. 0110specialize distinct_odd_prime_eisenstein_quotient_sum_identity x4
111. 0111specialize distinct_odd_prime_eisenstein_quotient_sum_identity x5
112. 0112specialize distinct_odd_prime_eisenstein_quotient_sum_identity x8
113. 0113specialize distinct_odd_prime_eisenstein_quotient_sum_identity x9
114. 0114specialize distinct_odd_prime_eisenstein_quotient_sum_identity x10
115. 0115specialize distinct_odd_prime_eisenstein_quotient_sum_identity x11
116. 0116specialize distinct_odd_prime_eisenstein_quotient_sum_identity x12
117. 0117specialize distinct_odd_prime_eisenstein_quotient_sum_identity x13
118. 0118specialize distinct_odd_prime_eisenstein_quotient_sum_identity x16
119. 0119specialize distinct_odd_prime_eisenstein_quotient_sum_identity x17
120. 0120specialize distinct_odd_prime_eisenstein_quotient_sum_identity x19
121. 0121specialize distinct_odd_prime_eisenstein_quotient_sum_identity x20
122. 0122specialize distinct_odd_prime_eisenstein_quotient_sum_identity x7
123. 0123specialize distinct_odd_prime_eisenstein_quotient_sum_identity x15
124. 0124apply distinct_odd_prime_eisenstein_quotient_sum_identity
125. 0125exact hpodd
126. 0126exact hqodd
127. 0127exact hp
128. 0128exact hq
129. 0129exact hpq
130. 0130exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_left
131. 0131exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_left
132. 0132exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_left
133. 0133exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_left
134. 0134exact hfirst_rectangle_witness_witness_witness_left
135. 0135exact hsecond_rectangle_witness_witness_witness_left
136. 0136exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
137. 0137exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
138. 0138exists x6
139. 0139exists x14
140. 0140exists x7
141. 0141exists x15
142. 0142split
143. 0143split
144. 0144exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
145. 0145exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
146. 0146split
147. 0147split
148. 0148exact hfirst_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
149. 0149exact hsecond_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
150. 0150exact hsum_identity