arbitrary_gauss_lemma_complete

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 hdouble : h + h = 2 * h
15. 0015trans h * 2
16. 0016simp [zero_add]
17. 0017specialize mul_comm h
18. 0018specialize mul_comm 2
19. 0019apply mul_comm
20. 0020have hgauss : exists e A R. ((exists ff_b_glb_multiplier_power ff_c_glb_multiplier_power. ((forall ff_i_glb_multiplier_power_repeat. (exists ff_lt_glb_multiplier_power_repeat_bound. ff_lt_glb_multiplier_power_repeat_bound + S ff_i_glb_multiplier_power_repeat = h) -> (((exists ff_h_glb_multiplier_power_repeat_decoded. ff_h_glb_multiplier_power_repeat_decoded + S (a) = S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_repeat_decoded. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_repeat_decoded * S ((S (ff_i_glb_multiplier_power_repeat)) * ff_c_glb_multiplier_power) + (a)))) /\ (exists ff_u_glb_multiplier_power_product ff_v_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_start. ff_h_glb_multiplier_power_product_start + S (1) = S ((S (0)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_start. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_start * S ((S (0)) * ff_v_glb_multiplier_power_product) + (1))) /\ ((((exists ff_h_glb_multiplier_power_product_terminal. ff_h_glb_multiplier_power_product_terminal + S (A) = S ((S (h)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_terminal. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_terminal * S ((S (h)) * ff_v_glb_multiplier_power_product) + (A))) /\ forall ff_i_glb_multiplier_power_product. (exists ff_lt_glb_multiplier_power_product_bound. ff_lt_glb_multiplier_power_product_bound + S ff_i_glb_multiplier_power_product = h) -> exists ff_p_glb_multiplier_power_product ff_r_glb_multiplier_power_product ff_s_glb_multiplier_power_product. ((((exists ff_h_glb_multiplier_power_product_factor. ff_h_glb_multiplier_power_product_factor + S (ff_p_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power)) /\ exists ff_q_glb_multiplier_power_product_factor. ff_b_glb_multiplier_power = ff_q_glb_multiplier_power_product_factor * S ((S (ff_i_glb_multiplier_power_product)) * ff_c_glb_multiplier_power) + (ff_p_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_partial. ff_h_glb_multiplier_power_product_partial + S (ff_r_glb_multiplier_power_product) = S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_partial. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_partial * S ((S (ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_r_glb_multiplier_power_product))) /\ ((((exists ff_h_glb_multiplier_power_product_successor. ff_h_glb_multiplier_power_product_successor + S (ff_s_glb_multiplier_power_product) = S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product)) /\ exists ff_q_glb_multiplier_power_product_successor. ff_u_glb_multiplier_power_product = ff_q_glb_multiplier_power_product_successor * S ((S (S ff_i_glb_multiplier_power_product)) * ff_v_glb_multiplier_power_product) + (ff_s_glb_multiplier_power_product))) /\ ff_s_glb_multiplier_power_product = ff_r_glb_multiplier_power_product * ff_p_glb_multiplier_power_product)))))))) /\ ((exists ff_b_glb_sign_power_expanded ff_c_glb_sign_power_expanded. ((forall ff_i_glb_sign_power_expanded_repeat. (exists ff_lt_glb_sign_power_expanded_repeat_bound. ff_lt_glb_sign_power_expanded_repeat_bound + S ff_i_glb_sign_power_expanded_repeat = e) -> (((exists ff_h_glb_sign_power_expanded_repeat_decoded. ff_h_glb_sign_power_expanded_repeat_decoded + S ((2 * h)) = S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_repeat_decoded. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_repeat_decoded * S ((S (ff_i_glb_sign_power_expanded_repeat)) * ff_c_glb_sign_power_expanded) + ((2 * h))))) /\ (exists ff_u_glb_sign_power_expanded_product ff_v_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_start. ff_h_glb_sign_power_expanded_product_start + S (1) = S ((S (0)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_start. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_start * S ((S (0)) * ff_v_glb_sign_power_expanded_product) + (1))) /\ ((((exists ff_h_glb_sign_power_expanded_product_terminal. ff_h_glb_sign_power_expanded_product_terminal + S (R) = S ((S (e)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_terminal. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_terminal * S ((S (e)) * ff_v_glb_sign_power_expanded_product) + (R))) /\ forall ff_i_glb_sign_power_expanded_product. (exists ff_lt_glb_sign_power_expanded_product_bound. ff_lt_glb_sign_power_expanded_product_bound + S ff_i_glb_sign_power_expanded_product = e) -> exists ff_p_glb_sign_power_expanded_product ff_r_glb_sign_power_expanded_product ff_s_glb_sign_power_expanded_product. ((((exists ff_h_glb_sign_power_expanded_product_factor. ff_h_glb_sign_power_expanded_product_factor + S (ff_p_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded)) /\ exists ff_q_glb_sign_power_expanded_product_factor. ff_b_glb_sign_power_expanded = ff_q_glb_sign_power_expanded_product_factor * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_c_glb_sign_power_expanded) + (ff_p_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_partial. ff_h_glb_sign_power_expanded_product_partial + S (ff_r_glb_sign_power_expanded_product) = S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_partial. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_partial * S ((S (ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_r_glb_sign_power_expanded_product))) /\ ((((exists ff_h_glb_sign_power_expanded_product_successor. ff_h_glb_sign_power_expanded_product_successor + S (ff_s_glb_sign_power_expanded_product) = S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product)) /\ exists ff_q_glb_sign_power_expanded_product_successor. ff_u_glb_sign_power_expanded_product = ff_q_glb_sign_power_expanded_product_successor * S ((S (S ff_i_glb_sign_power_expanded_product)) * ff_v_glb_sign_power_expanded_product) + (ff_s_glb_sign_power_expanded_product))) /\ ff_s_glb_sign_power_expanded_product = ff_r_glb_sign_power_expanded_product * ff_p_glb_sign_power_expanded_product)))))))) /\ ((exists mb mc sb sc. ((forall gsp_index_glb_signed_prefix. (exists gsp_lt_gap_glb_signed_prefix_index_bound. gsp_lt_gap_glb_signed_prefix_index_bound + S gsp_index_glb_signed_prefix = h) -> (exists gsp_value_glb_signed_prefix_entry gsp_magnitude_glb_signed_prefix_entry gsp_sign_glb_signed_prefix_entry. (((exists ff_h_gsp_glb_signed_prefix_entry_source. ff_h_gsp_glb_signed_prefix_entry_source + S (gsp_value_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * c)) /\ exists ff_q_gsp_glb_signed_prefix_entry_source. b = ff_q_gsp_glb_signed_prefix_entry_source * S ((S (gsp_index_glb_signed_prefix)) * c) + (gsp_value_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_magnitude. ff_h_gsp_glb_signed_prefix_entry_magnitude + S (gsp_magnitude_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * mc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_magnitude. mb = ff_q_gsp_glb_signed_prefix_entry_magnitude * S ((S (gsp_index_glb_signed_prefix)) * mc) + (gsp_magnitude_glb_signed_prefix_entry))) /\ ((((exists ff_h_gsp_glb_signed_prefix_entry_sign. ff_h_gsp_glb_signed_prefix_entry_sign + S (gsp_sign_glb_signed_prefix_entry) = S ((S (gsp_index_glb_signed_prefix)) * sc)) /\ exists ff_q_gsp_glb_signed_prefix_entry_sign. sb = ff_q_gsp_glb_signed_prefix_entry_sign * S ((S (gsp_index_glb_signed_prefix)) * sc) + (gsp_sign_glb_signed_prefix_entry))) /\ ((exists gsp_lt_gap_glb_signed_prefix_entry_positive. gsp_lt_gap_glb_signed_prefix_entry_positive + S 0 = gsp_magnitude_glb_signed_prefix_entry) /\ ((exists gsp_le_gap_glb_signed_prefix_entry_bounded. gsp_le_gap_glb_signed_prefix_entry_bounded + gsp_magnitude_glb_signed_prefix_entry = h) /\ ((gsp_sign_glb_signed_prefix_entry = 0 \/ gsp_sign_glb_signed_prefix_entry = 1) /\ (((gsp_sign_glb_signed_prefix_entry = 0 /\ (exists gsp_mod_left_glb_signed_prefix_entry_lower gsp_mod_right_glb_signed_prefix_entry_lower. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_lower = (gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_lower)) \/ (gsp_sign_glb_signed_prefix_entry = 1 /\ (exists gsp_mod_left_glb_signed_prefix_entry_reflected gsp_mod_right_glb_signed_prefix_entry_reflected. (a * gsp_value_glb_signed_prefix_entry) + p * gsp_mod_left_glb_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_glb_signed_prefix_entry) + p * gsp_mod_right_glb_signed_prefix_entry_reflected))))))))))) /\ (((exists ff_u_glb_count_sum ff_v_glb_count_sum. ((((exists ff_h_glb_count_sum_start. ff_h_glb_count_sum_start + S (0) = S ((S (0)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_start. ff_u_glb_count_sum = ff_q_glb_count_sum_start * S ((S (0)) * ff_v_glb_count_sum) + (0))) /\ ((((exists ff_h_glb_count_sum_terminal. ff_h_glb_count_sum_terminal + S (e) = S ((S (h)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_terminal. ff_u_glb_count_sum = ff_q_glb_count_sum_terminal * S ((S (h)) * ff_v_glb_count_sum) + (e))) /\ forall ff_i_glb_count_sum. (exists ff_lt_glb_count_sum_bound. ff_lt_glb_count_sum_bound + S ff_i_glb_count_sum = h) -> exists ff_a_glb_count_sum ff_r_glb_count_sum ff_s_glb_count_sum. ((((exists ff_h_glb_count_sum_summand. ff_h_glb_count_sum_summand + S (ff_a_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * sc)) /\ exists ff_q_glb_count_sum_summand. sb = ff_q_glb_count_sum_summand * S ((S (ff_i_glb_count_sum)) * sc) + (ff_a_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_partial. ff_h_glb_count_sum_partial + S (ff_r_glb_count_sum) = S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_partial. ff_u_glb_count_sum = ff_q_glb_count_sum_partial * S ((S (ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_r_glb_count_sum))) /\ ((((exists ff_h_glb_count_sum_successor. ff_h_glb_count_sum_successor + S (ff_s_glb_count_sum) = S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum)) /\ exists ff_q_glb_count_sum_successor. ff_u_glb_count_sum = ff_q_glb_count_sum_successor * S ((S (S ff_i_glb_count_sum)) * ff_v_glb_count_sum) + (ff_s_glb_count_sum))) /\ ff_s_glb_count_sum = ff_r_glb_count_sum + ff_a_glb_count_sum)))))) /\ (forall ff_i_glb_count_bits. (exists ff_lt_glb_count_bits_bound. ff_lt_glb_count_bits_bound + S ff_i_glb_count_bits = h) -> exists ff_bit_glb_count_bits. ((((exists ff_h_glb_count_bits_decoded. ff_h_glb_count_bits_decoded + S (ff_bit_glb_count_bits) = S ((S (ff_i_glb_count_bits)) * sc)) /\ exists ff_q_glb_count_bits_decoded. sb = ff_q_glb_count_bits_decoded * S ((S (ff_i_glb_count_bits)) * sc) + (ff_bit_glb_count_bits))) /\ (ff_bit_glb_count_bits = 0 \/ ff_bit_glb_count_bits = 1))))))) /\ (exists wpp_mod_left_glb_a_mod_r wpp_mod_right_glb_a_mod_r. (A) + p * wpp_mod_left_glb_a_mod_r = (R) + p * wpp_mod_right_glb_a_mod_r))))
21. 0021specialize gauss_lemma_power_congruence_exists p
22. 0022specialize gauss_lemma_power_congruence_exists h
23. 0023specialize gauss_lemma_power_congruence_exists a
24. 0024specialize gauss_lemma_power_congruence_exists b
25. 0025specialize gauss_lemma_power_congruence_exists c
26. 0026apply gauss_lemma_power_congruence_exists
27. 0027exact hpodd
28. 0028exact hprime
29. 0029exact hnotdiv
30. 0030exact hhalf
31. 0031cases hgauss
32. 0032cases hgauss_witness
33. 0033cases hgauss_witness_witness
34. 0034cases hgauss_witness_witness_witness
35. 0035cases hgauss_witness_witness_witness_right
36. 0036cases hgauss_witness_witness_witness_right_right
37. 0037have heuler : (((((exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one)) /\ ((exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)))) /\ ((~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor)) /\ ((exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres))))
38. 0038specialize arbitrary_euler_criterion_complete p
39. 0039specialize arbitrary_euler_criterion_complete a
40. 0040specialize arbitrary_euler_criterion_complete (2 * h)
41. 0041specialize arbitrary_euler_criterion_complete h
42. 0042specialize arbitrary_euler_criterion_complete x1
43. 0043apply arbitrary_euler_criterion_complete
44. 0044exact hpsucc
45. 0045exact hprime
46. 0046exact hnotdiv
47. 0047symm
48. 0048exact hdouble
49. 0049exact hgauss_witness_witness_witness_left
50. 0050cases heuler
51. 0051cases heuler_left
52. 0052cases heuler_right
53. 0053have hbridge : (((exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one)) /\ ((exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> (exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor)))
54. 0054specialize pow_predecessor_parity_mod p
55. 0055specialize pow_predecessor_parity_mod (2 * h)
56. 0056specialize pow_predecessor_parity_mod x
57. 0057specialize pow_predecessor_parity_mod x2
58. 0058apply pow_predecessor_parity_mod
59. 0059exact hpsucc
60. 0060exact hgauss_witness_witness_witness_right_left
61. 0061cases hbridge
62. 0062have hseparation : ~(exists wpp_mod_left_glb_one_mod_predecessor wpp_mod_right_glb_one_mod_predecessor. (1) + p * wpp_mod_left_glb_one_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_one_mod_predecessor)
63. 0063intro hcollision
64. 0064specialize odd_prime_one_not_mod_predecessor p
65. 0065specialize odd_prime_one_not_mod_predecessor (2 * h)
66. 0066specialize odd_prime_one_not_mod_predecessor h
67. 0067apply odd_prime_one_not_mod_predecessor
68. 0068exact hpsucc
69. 0069exact hprime
70. 0070symm
71. 0071exact hdouble
72. 0072exact hcollision
73. 0073have hqres_even : (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even)
74. 0074intro hqres
75. 0075specialize parity_cases x
76. 0076cases parity_cases
77. 0077cases parity_cases_witness
78. 0078exists x3
79. 0079exact parity_cases_witness_left
80. 0080exfalso
81. 0081apply hseparation
82. 0082have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
83. 0083apply heuler_left_left
84. 0084exact hqres
85. 0085have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
86. 0086specialize mod_eq_symm p
87. 0087specialize mod_eq_symm x1
88. 0088specialize mod_eq_symm 1
89. 0089apply mod_eq_symm
90. 0090exact hAone
91. 0091have honeR : exists wpp_mod_left_glb_local_one_mod_r wpp_mod_right_glb_local_one_mod_r. (1) + p * wpp_mod_left_glb_local_one_mod_r = (x2) + p * wpp_mod_right_glb_local_one_mod_r
92. 0092specialize mod_eq_trans p
93. 0093specialize mod_eq_trans 1
94. 0094specialize mod_eq_trans x1
95. 0095specialize mod_eq_trans x2
96. 0096apply mod_eq_trans
97. 0097exact honeA
98. 0098exact hgauss_witness_witness_witness_right_right_right
99. 0099have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
100. 0100apply hbridge_right
101. 0101exists x3
102. 0102exact parity_cases_witness_right
103. 0103specialize mod_eq_trans p
104. 0104specialize mod_eq_trans 1
105. 0105specialize mod_eq_trans x2
106. 0106specialize mod_eq_trans (2 * h)
107. 0107apply mod_eq_trans
108. 0108exact honeR
109. 0109exact hRpred
110. 0110have heven_qres : (exists gs_even_glb_local_even. x = 2 * gs_even_glb_local_even) -> (exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
111. 0111intro heven
112. 0112have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
113. 0113apply hbridge_left
114. 0114exact heven
115. 0115have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
116. 0116specialize mod_eq_trans p
117. 0117specialize mod_eq_trans x1
118. 0118specialize mod_eq_trans x2
119. 0119specialize mod_eq_trans 1
120. 0120apply mod_eq_trans
121. 0121exact hgauss_witness_witness_witness_right_right_right
122. 0122exact hRone
123. 0123apply heuler_left_right
124. 0124exact hAone
125. 0125have hnonres_odd : ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres) -> (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1)
126. 0126intro hnonres
127. 0127specialize parity_cases x
128. 0128cases parity_cases
129. 0129cases parity_cases_witness
130. 0130exfalso
131. 0131apply hseparation
132. 0132have hRone : exists wpp_mod_left_glb_local_r_mod_one wpp_mod_right_glb_local_r_mod_one. (x2) + p * wpp_mod_left_glb_local_r_mod_one = (1) + p * wpp_mod_right_glb_local_r_mod_one
133. 0133apply hbridge_left
134. 0134exists x3
135. 0135exact parity_cases_witness_left
136. 0136have hAone : exists wpp_mod_left_glb_local_a_mod_one wpp_mod_right_glb_local_a_mod_one. (x1) + p * wpp_mod_left_glb_local_a_mod_one = (1) + p * wpp_mod_right_glb_local_a_mod_one
137. 0137specialize mod_eq_trans p
138. 0138specialize mod_eq_trans x1
139. 0139specialize mod_eq_trans x2
140. 0140specialize mod_eq_trans 1
141. 0141apply mod_eq_trans
142. 0142exact hgauss_witness_witness_witness_right_right_right
143. 0143exact hRone
144. 0144have honeA : exists wpp_mod_left_glb_local_one_mod_a wpp_mod_right_glb_local_one_mod_a. (1) + p * wpp_mod_left_glb_local_one_mod_a = (x1) + p * wpp_mod_right_glb_local_one_mod_a
145. 0145specialize mod_eq_symm p
146. 0146specialize mod_eq_symm x1
147. 0147specialize mod_eq_symm 1
148. 0148apply mod_eq_symm
149. 0149exact hAone
150. 0150have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
151. 0151apply heuler_right_left
152. 0152exact hnonres
153. 0153specialize mod_eq_trans p
154. 0154specialize mod_eq_trans 1
155. 0155specialize mod_eq_trans x1
156. 0156specialize mod_eq_trans (2 * h)
157. 0157apply mod_eq_trans
158. 0158exact honeA
159. 0159exact hApred
160. 0160exists x3
161. 0161exact parity_cases_witness_right
162. 0162have hodd_nonres : (exists gs_odd_glb_local_odd. x = 2 * gs_odd_glb_local_odd + 1) -> ~(exists qr_x_glb_qres. exists qr_u_glb_qres qr_v_glb_qres. qr_x_glb_qres * qr_x_glb_qres + p * qr_u_glb_qres = a + p * qr_v_glb_qres)
163. 0163intro hodd
164. 0164have hRpred : exists wpp_mod_left_glb_local_r_mod_predecessor wpp_mod_right_glb_local_r_mod_predecessor. (x2) + p * wpp_mod_left_glb_local_r_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_r_mod_predecessor
165. 0165apply hbridge_right
166. 0166exact hodd
167. 0167have hApred : exists wpp_mod_left_glb_local_a_mod_predecessor wpp_mod_right_glb_local_a_mod_predecessor. (x1) + p * wpp_mod_left_glb_local_a_mod_predecessor = (2 * h) + p * wpp_mod_right_glb_local_a_mod_predecessor
168. 0168specialize mod_eq_trans p
169. 0169specialize mod_eq_trans x1
170. 0170specialize mod_eq_trans x2
171. 0171specialize mod_eq_trans (2 * h)
172. 0172apply mod_eq_trans
173. 0173exact hgauss_witness_witness_witness_right_right_right
174. 0174exact hRpred
175. 0175intro hqres
176. 0176apply heuler_right_right
177. 0177exact hApred
178. 0178exact hqres
179. 0179exists x
180. 0180split
181. 0181exact hgauss_witness_witness_witness_right_right_left
182. 0182split
183. 0183split
184. 0184exact hqres_even
185. 0185exact heven_qres
186. 0186split
187. 0187exact hnonres_odd
188. 0188exact hodd_nonres