PA007C

gauss_signed_half_magnitude_injective

Alpha v16 checked-use theorem · independently closed; not Stable

The positive signed-half magnitude prefix is injective over the full beta-coded half range.

Exact expanded PA statement

forall p h a b c mb mc sb sc. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_collision_prime gsp_prime_right_collision_prime. p = gsp_prime_left_collision_prime * gsp_prime_right_collision_prime -> gsp_prime_left_collision_prime = 1 \/ gsp_prime_right_collision_prime = 1)) -> (~(exists gsp_divisor_factor_collision_multiplier. a = p * gsp_divisor_factor_collision_multiplier)) -> (forall gsp_range_index_injective_source. (exists gsp_lt_gap_injective_source_range_bound. gsp_lt_gap_injective_source_range_bound + S gsp_range_index_injective_source = h) -> (((exists gsp_beta_height_injective_source_range_entry. gsp_beta_height_injective_source_range_entry + S (1 + gsp_range_index_injective_source) = S ((S (gsp_range_index_injective_source)) * c)) /\ exists gsp_beta_quotient_injective_source_range_entry. b = gsp_beta_quotient_injective_source_range_entry * S ((S (gsp_range_index_injective_source)) * c) + (1 + gsp_range_index_injective_source)))) -> (forall gsp_index_injective_signed_source. (exists gsp_lt_gap_injective_signed_source_index_bound. gsp_lt_gap_injective_signed_source_index_bound + S gsp_index_injective_signed_source = h) -> (exists gsp_value_injective_signed_source_entry gsp_magnitude_injective_signed_source_entry gsp_sign_injective_signed_source_entry. (((exists ff_h_gsp_injective_signed_source_entry_source. ff_h_gsp_injective_signed_source_entry_source + S (gsp_value_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * c)) /\ exists ff_q_gsp_injective_signed_source_entry_source. b = ff_q_gsp_injective_signed_source_entry_source * S ((S (gsp_index_injective_signed_source)) * c) + (gsp_value_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_magnitude. ff_h_gsp_injective_signed_source_entry_magnitude + S (gsp_magnitude_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * mc)) /\ exists ff_q_gsp_injective_signed_source_entry_magnitude. mb = ff_q_gsp_injective_signed_source_entry_magnitude * S ((S (gsp_index_injective_signed_source)) * mc) + (gsp_magnitude_injective_signed_source_entry))) /\ ((((exists ff_h_gsp_injective_signed_source_entry_sign. ff_h_gsp_injective_signed_source_entry_sign + S (gsp_sign_injective_signed_source_entry) = S ((S (gsp_index_injective_signed_source)) * sc)) /\ exists ff_q_gsp_injective_signed_source_entry_sign. sb = ff_q_gsp_injective_signed_source_entry_sign * S ((S (gsp_index_injective_signed_source)) * sc) + (gsp_sign_injective_signed_source_entry))) /\ ((exists gsp_lt_gap_injective_signed_source_entry_positive. gsp_lt_gap_injective_signed_source_entry_positive + S 0 = gsp_magnitude_injective_signed_source_entry) /\ ((exists gsp_le_gap_injective_signed_source_entry_bounded. gsp_le_gap_injective_signed_source_entry_bounded + gsp_magnitude_injective_signed_source_entry = h) /\ ((gsp_sign_injective_signed_source_entry = 0 \/ gsp_sign_injective_signed_source_entry = 1) /\ (((gsp_sign_injective_signed_source_entry = 0 /\ (exists gsp_mod_left_injective_signed_source_entry_lower gsp_mod_right_injective_signed_source_entry_lower. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_lower = (gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_lower)) \/ (gsp_sign_injective_signed_source_entry = 1 /\ (exists gsp_mod_left_injective_signed_source_entry_reflected gsp_mod_right_injective_signed_source_entry_reflected. (a * gsp_value_injective_signed_source_entry) + p * gsp_mod_left_injective_signed_source_entry_reflected = ((2 * h) * gsp_magnitude_injective_signed_source_entry) + p * gsp_mod_right_injective_signed_source_entry_reflected))))))))))) -> (forall fp_i_signed_magnitude_injective fp_j_signed_magnitude_injective fp_value_signed_magnitude_injective. (exists fp_gap_signed_magnitude_injective_i. fp_gap_signed_magnitude_injective_i + S fp_i_signed_magnitude_injective = h) -> (exists fp_gap_signed_magnitude_injective_j. fp_gap_signed_magnitude_injective_j + S fp_j_signed_magnitude_injective = h) -> (((exists ff_h_signed_magnitude_injective_left. ff_h_signed_magnitude_injective_left + S (fp_value_signed_magnitude_injective) = S ((S (fp_i_signed_magnitude_injective)) * mc)) /\ exists ff_q_signed_magnitude_injective_left. mb = ff_q_signed_magnitude_injective_left * S ((S (fp_i_signed_magnitude_injective)) * mc) + (fp_value_signed_magnitude_injective))) -> (((exists ff_h_signed_magnitude_injective_right. ff_h_signed_magnitude_injective_right + S (fp_value_signed_magnitude_injective) = S ((S (fp_j_signed_magnitude_injective)) * mc)) /\ exists ff_q_signed_magnitude_injective_right. mb = ff_q_signed_magnitude_injective_right * S ((S (fp_j_signed_magnitude_injective)) * mc) + (fp_value_signed_magnitude_injective))) -> fp_i_signed_magnitude_injective = fp_j_signed_magnitude_injective)

Structural proof guide

Generated structural guide

The positive signed-half magnitude prefix is injective over the full beta-coded half range.

Use the direct prerequisites beta_at_unique, beta_half_range_entry_bounds, beta_range_entry_eq, add_succ_left, zero_add, add_le_add_right, add_le_add_left, le_trans, mul_succ_left, mul_zero_left, lt_of_le_of_lt, add_eq_zero_left, add_comm, gauss_same_sign_scaled_source_unique, gauss_mixed_sign_scaled_source_impossible, beta_range_injective as previously established PA formulas.

The proof proceeds by case analysis (29), intermediate claims (24), equality transport (10), certified simplification (1).

Referenced ingredients

PA002F beta_at_unique PA0034 beta_half_range_entry_bounds PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000G mul_succ_left PA000D mul_zero_left PA0033 lt_of_le_of_lt PA000J add_eq_zero_left PA000F add_comm PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA003T beta_range_injective

Proof neighborhood

Direct dependencies

PA002F beta_at_unique PA0034 beta_half_range_entry_bounds PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000G mul_succ_left PA000D mul_zero_left PA0033 lt_of_le_of_lt PA000J add_eq_zero_left PA000F add_comm PA007A gauss_same_sign_scaled_source_unique PA007B gauss_mixed_sign_scaled_source_impossible PA003T beta_range_injective

Direct dependents

PA0085 gauss_lemma_power_congruence_exists PA00D0 gauss_signed_half_magnitude_sum_equals_half_sum

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 mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro hpodd
  11. 0011intro hp
  12. 0012intro hnotdiv
  13. 0013intro hrange
  14. 0014intro hprefix
  15. 0015intro i
  16. 0016intro j
  17. 0017intro m
  18. 0018intro hi
  19. 0019intro hj
  20. 0020intro hmi
  21. 0021intro hmj
  22. 0022have hentryi : exists gsp_value_injective_entry_i gsp_magnitude_injective_entry_i gsp_sign_injective_entry_i. (((exists ff_h_gsp_injective_entry_i_source. ff_h_gsp_injective_entry_i_source + S (gsp_value_injective_entry_i) = S ((S (i)) * c)) /\ exists ff_q_gsp_injective_entry_i_source. b = ff_q_gsp_injective_entry_i_source * S ((S (i)) * c) + (gsp_value_injective_entry_i))) /\ ((((exists ff_h_gsp_injective_entry_i_magnitude. ff_h_gsp_injective_entry_i_magnitude + S (gsp_magnitude_injective_entry_i) = S ((S (i)) * mc)) /\ exists ff_q_gsp_injective_entry_i_magnitude. mb = ff_q_gsp_injective_entry_i_magnitude * S ((S (i)) * mc) + (gsp_magnitude_injective_entry_i))) /\ ((((exists ff_h_gsp_injective_entry_i_sign. ff_h_gsp_injective_entry_i_sign + S (gsp_sign_injective_entry_i) = S ((S (i)) * sc)) /\ exists ff_q_gsp_injective_entry_i_sign. sb = ff_q_gsp_injective_entry_i_sign * S ((S (i)) * sc) + (gsp_sign_injective_entry_i))) /\ ((exists gsp_lt_gap_injective_entry_i_positive. gsp_lt_gap_injective_entry_i_positive + S 0 = gsp_magnitude_injective_entry_i) /\ ((exists gsp_le_gap_injective_entry_i_bounded. gsp_le_gap_injective_entry_i_bounded + gsp_magnitude_injective_entry_i = h) /\ ((gsp_sign_injective_entry_i = 0 \/ gsp_sign_injective_entry_i = 1) /\ (((gsp_sign_injective_entry_i = 0 /\ (exists gsp_mod_left_injective_entry_i_lower gsp_mod_right_injective_entry_i_lower. (a * gsp_value_injective_entry_i) + p * gsp_mod_left_injective_entry_i_lower = (gsp_magnitude_injective_entry_i) + p * gsp_mod_right_injective_entry_i_lower)) \/ (gsp_sign_injective_entry_i = 1 /\ (exists gsp_mod_left_injective_entry_i_reflected gsp_mod_right_injective_entry_i_reflected. (a * gsp_value_injective_entry_i) + p * gsp_mod_left_injective_entry_i_reflected = ((2 * h) * gsp_magnitude_injective_entry_i) + p * gsp_mod_right_injective_entry_i_reflected)))))))))
  23. 0023specialize hprefix i
  24. 0024apply hprefix
  25. 0025exact hi
  26. 0026cases hentryi
  27. 0027cases hentryi_witness
  28. 0028cases hentryi_witness_witness
  29. 0029cases hentryi_witness_witness_witness
  30. 0030cases hentryi_witness_witness_witness_right
  31. 0031cases hentryi_witness_witness_witness_right_right
  32. 0032cases hentryi_witness_witness_witness_right_right_right
  33. 0033cases hentryi_witness_witness_witness_right_right_right_right
  34. 0034cases hentryi_witness_witness_witness_right_right_right_right_right
  35. 0035have hentryj : exists gsp_value_injective_entry_j gsp_magnitude_injective_entry_j gsp_sign_injective_entry_j. (((exists ff_h_gsp_injective_entry_j_source. ff_h_gsp_injective_entry_j_source + S (gsp_value_injective_entry_j) = S ((S (j)) * c)) /\ exists ff_q_gsp_injective_entry_j_source. b = ff_q_gsp_injective_entry_j_source * S ((S (j)) * c) + (gsp_value_injective_entry_j))) /\ ((((exists ff_h_gsp_injective_entry_j_magnitude. ff_h_gsp_injective_entry_j_magnitude + S (gsp_magnitude_injective_entry_j) = S ((S (j)) * mc)) /\ exists ff_q_gsp_injective_entry_j_magnitude. mb = ff_q_gsp_injective_entry_j_magnitude * S ((S (j)) * mc) + (gsp_magnitude_injective_entry_j))) /\ ((((exists ff_h_gsp_injective_entry_j_sign. ff_h_gsp_injective_entry_j_sign + S (gsp_sign_injective_entry_j) = S ((S (j)) * sc)) /\ exists ff_q_gsp_injective_entry_j_sign. sb = ff_q_gsp_injective_entry_j_sign * S ((S (j)) * sc) + (gsp_sign_injective_entry_j))) /\ ((exists gsp_lt_gap_injective_entry_j_positive. gsp_lt_gap_injective_entry_j_positive + S 0 = gsp_magnitude_injective_entry_j) /\ ((exists gsp_le_gap_injective_entry_j_bounded. gsp_le_gap_injective_entry_j_bounded + gsp_magnitude_injective_entry_j = h) /\ ((gsp_sign_injective_entry_j = 0 \/ gsp_sign_injective_entry_j = 1) /\ (((gsp_sign_injective_entry_j = 0 /\ (exists gsp_mod_left_injective_entry_j_lower gsp_mod_right_injective_entry_j_lower. (a * gsp_value_injective_entry_j) + p * gsp_mod_left_injective_entry_j_lower = (gsp_magnitude_injective_entry_j) + p * gsp_mod_right_injective_entry_j_lower)) \/ (gsp_sign_injective_entry_j = 1 /\ (exists gsp_mod_left_injective_entry_j_reflected gsp_mod_right_injective_entry_j_reflected. (a * gsp_value_injective_entry_j) + p * gsp_mod_left_injective_entry_j_reflected = ((2 * h) * gsp_magnitude_injective_entry_j) + p * gsp_mod_right_injective_entry_j_reflected)))))))))
  36. 0036specialize hprefix j
  37. 0037apply hprefix
  38. 0038exact hj
  39. 0039cases hentryj
  40. 0040cases hentryj_witness
  41. 0041cases hentryj_witness_witness
  42. 0042cases hentryj_witness_witness_witness
  43. 0043cases hentryj_witness_witness_witness_right
  44. 0044cases hentryj_witness_witness_witness_right_right
  45. 0045cases hentryj_witness_witness_witness_right_right_right
  46. 0046cases hentryj_witness_witness_witness_right_right_right_right
  47. 0047cases hentryj_witness_witness_witness_right_right_right_right_right
  48. 0048have hmagi : m = x1
  49. 0049specialize beta_at_unique mb
  50. 0050specialize beta_at_unique mc
  51. 0051specialize beta_at_unique i
  52. 0052specialize beta_at_unique m
  53. 0053specialize beta_at_unique x1
  54. 0054apply beta_at_unique
  55. 0055exact hmi
  56. 0056exact hentryi_witness_witness_witness_right_left
  57. 0057have hmagj : m = x4
  58. 0058specialize beta_at_unique mb
  59. 0059specialize beta_at_unique mc
  60. 0060specialize beta_at_unique j
  61. 0061specialize beta_at_unique m
  62. 0062specialize beta_at_unique x4
  63. 0063apply beta_at_unique
  64. 0064exact hmj
  65. 0065exact hentryj_witness_witness_witness_right_left
  66. 0066rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
  67. 0067rewrite <- hmagi at hentryi_witness_witness_witness_right_right_right_right_right_right
  68. 0068rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
  69. 0069rewrite <- hmagj at hentryj_witness_witness_witness_right_right_right_right_right_right
  70. 0070have hisigned : ((x2 = 0 /\ (exists gmp_mod_left_injective_i_lower gmp_mod_right_injective_i_lower. (a * x) + p * gmp_mod_left_injective_i_lower = (m) + p * gmp_mod_right_injective_i_lower)) \/ (x2 = 1 /\ (exists gmp_mod_left_injective_i_reflected gmp_mod_right_injective_i_reflected. (a * x) + p * gmp_mod_left_injective_i_reflected = ((2 * h) * m) + p * gmp_mod_right_injective_i_reflected)))
  71. 0071exact hentryi_witness_witness_witness_right_right_right_right_right_right
  72. 0072have hjsigned : ((x5 = 0 /\ (exists gmp_mod_left_injective_j_lower gmp_mod_right_injective_j_lower. (a * x3) + p * gmp_mod_left_injective_j_lower = (m) + p * gmp_mod_right_injective_j_lower)) \/ (x5 = 1 /\ (exists gmp_mod_left_injective_j_reflected gmp_mod_right_injective_j_reflected. (a * x3) + p * gmp_mod_left_injective_j_reflected = ((2 * h) * m) + p * gmp_mod_right_injective_j_reflected)))
  73. 0073exact hentryj_witness_witness_witness_right_right_right_right_right_right
  74. 0074have hxbounds : (~(x = 0) /\ (exists gsp_lt_gap_injective_x_bound. gsp_lt_gap_injective_x_bound + S x = p))
  75. 0075specialize beta_half_range_entry_bounds p
  76. 0076specialize beta_half_range_entry_bounds h
  77. 0077specialize beta_half_range_entry_bounds b
  78. 0078specialize beta_half_range_entry_bounds c
  79. 0079specialize beta_half_range_entry_bounds i
  80. 0080specialize beta_half_range_entry_bounds x
  81. 0081apply beta_half_range_entry_bounds
  82. 0082exact hpodd
  83. 0083exact hrange
  84. 0084exact hi
  85. 0085exact hentryi_witness_witness_witness_left
  86. 0086have hybounds : (~(x3 = 0) /\ (exists gsp_lt_gap_injective_y_bound. gsp_lt_gap_injective_y_bound + S x3 = p))
  87. 0087specialize beta_half_range_entry_bounds p
  88. 0088specialize beta_half_range_entry_bounds h
  89. 0089specialize beta_half_range_entry_bounds b
  90. 0090specialize beta_half_range_entry_bounds c
  91. 0091specialize beta_half_range_entry_bounds j
  92. 0092specialize beta_half_range_entry_bounds x3
  93. 0093apply beta_half_range_entry_bounds
  94. 0094exact hpodd
  95. 0095exact hrange
  96. 0096exact hj
  97. 0097exact hentryj_witness_witness_witness_left
  98. 0098cases hxbounds
  99. 0099cases hybounds
  100. 0100have hxvalue : x = 1 + i
  101. 0101specialize beta_range_entry_eq b
  102. 0102specialize beta_range_entry_eq c
  103. 0103specialize beta_range_entry_eq 1
  104. 0104specialize beta_range_entry_eq h
  105. 0105specialize beta_range_entry_eq i
  106. 0106specialize beta_range_entry_eq x
  107. 0107apply beta_range_entry_eq
  108. 0108exact hrange
  109. 0109exact hi
  110. 0110exact hentryi_witness_witness_witness_left
  111. 0111have hyvalue : x3 = 1 + j
  112. 0112specialize beta_range_entry_eq b
  113. 0113specialize beta_range_entry_eq c
  114. 0114specialize beta_range_entry_eq 1
  115. 0115specialize beta_range_entry_eq h
  116. 0116specialize beta_range_entry_eq j
  117. 0117specialize beta_range_entry_eq x3
  118. 0118apply beta_range_entry_eq
  119. 0119exact hrange
  120. 0120exact hj
  121. 0121exact hentryj_witness_witness_witness_left
  122. 0122have honei : 1 + i = S i
  123. 0123trans S (0 + i)
  124. 0124specialize add_succ_left 0
  125. 0125specialize add_succ_left i
  126. 0126exact add_succ_left
  127. 0127congr
  128. 0128specialize zero_add i
  129. 0129exact zero_add
  130. 0130have honej : 1 + j = S j
  131. 0131trans S (0 + j)
  132. 0132specialize add_succ_left 0
  133. 0133specialize add_succ_left j
  134. 0134exact add_succ_left
  135. 0135congr
  136. 0136specialize zero_add j
  137. 0137exact zero_add
  138. 0138have hxle : exists gsp_le_gap_injective_x_le_half. gsp_le_gap_injective_x_le_half + x = h
  139. 0139rewrite hxvalue
  140. 0140rewrite honei
  141. 0141exact hi
  142. 0142have hyle : exists gsp_le_gap_injective_y_le_half. gsp_le_gap_injective_y_le_half + x3 = h
  143. 0143rewrite hyvalue
  144. 0144rewrite honej
  145. 0145exact hj
  146. 0146have hsum_first : exists gmp_sum_first_gap. gmp_sum_first_gap + (x + x3) = h + x3
  147. 0147specialize add_le_add_right x
  148. 0148specialize add_le_add_right h
  149. 0149specialize add_le_add_right x3
  150. 0150apply add_le_add_right
  151. 0151exact hxle
  152. 0152have hsum_second : exists gmp_sum_second_gap. gmp_sum_second_gap + (h + x3) = h + h
  153. 0153specialize add_le_add_left x3
  154. 0154specialize add_le_add_left h
  155. 0155specialize add_le_add_left h
  156. 0156apply add_le_add_left
  157. 0157exact hyle
  158. 0158have hsum_le_double : exists gmp_sum_double_gap. gmp_sum_double_gap + (x + x3) = h + h
  159. 0159specialize le_trans (x + x3)
  160. 0160specialize le_trans (h + x3)
  161. 0161specialize le_trans (h + h)
  162. 0162apply le_trans
  163. 0163exact hsum_first
  164. 0164exact hsum_second
  165. 0165have hdouble_below : exists gmp_double_below_gap. gmp_double_below_gap + S (h + h) = p
  166. 0166exists 0
  167. 0167rewrite hpodd
  168. 0168simp [mul_succ_left, mul_zero_left, zero_add, add_succ_left]
  169. 0169have hsum_bound : exists gsp_lt_gap_injective_sum_bound. gsp_lt_gap_injective_sum_bound + S (x + x3) = p
  170. 0170specialize lt_of_le_of_lt (x + x3)
  171. 0171specialize lt_of_le_of_lt (h + h)
  172. 0172specialize lt_of_le_of_lt p
  173. 0173apply lt_of_le_of_lt
  174. 0174exact hsum_le_double
  175. 0175exact hdouble_below
  176. 0176have hsum_nonzero : ~(x + x3 = 0)
  177. 0177intro hsumzero
  178. 0178apply hxbounds_left
  179. 0179specialize add_eq_zero_left x
  180. 0180specialize add_eq_zero_left x3
  181. 0181apply add_eq_zero_left
  182. 0182exact hsumzero
  183. 0183have hsumcomm : x3 + x = x + x3
  184. 0184specialize add_comm x3
  185. 0185specialize add_comm x
  186. 0186exact add_comm
  187. 0187have hreverse_sum_bound : exists gsp_lt_gap_injective_reverse_sum_bound. gsp_lt_gap_injective_reverse_sum_bound + S (x3 + x) = p
  188. 0188rewrite hsumcomm
  189. 0189exact hsum_bound
  190. 0190have hreverse_sum_nonzero : ~(x3 + x = 0)
  191. 0191intro hreversezero
  192. 0192apply hsum_nonzero
  193. 0193trans x3 + x
  194. 0194symm
  195. 0195exact hsumcomm
  196. 0196exact hreversezero
  197. 0197have hsourceeq : x = x3
  198. 0198cases hisigned
  199. 0199cases hisigned_left
  200. 0200cases hjsigned
  201. 0201cases hjsigned_left
  202. 0202specialize gauss_same_sign_scaled_source_unique p
  203. 0203specialize gauss_same_sign_scaled_source_unique h
  204. 0204specialize gauss_same_sign_scaled_source_unique a
  205. 0205specialize gauss_same_sign_scaled_source_unique x
  206. 0206specialize gauss_same_sign_scaled_source_unique x3
  207. 0207specialize gauss_same_sign_scaled_source_unique m
  208. 0208apply gauss_same_sign_scaled_source_unique
  209. 0209exact hp
  210. 0210exact hnotdiv
  211. 0211exact hxbounds_right
  212. 0212exact hybounds_right
  213. 0213left
  214. 0214split
  215. 0215exact hisigned_left_right
  216. 0216exact hjsigned_left_right
  217. 0217cases hjsigned_right
  218. 0218exfalso
  219. 0219specialize gauss_mixed_sign_scaled_source_impossible p
  220. 0220specialize gauss_mixed_sign_scaled_source_impossible h
  221. 0221specialize gauss_mixed_sign_scaled_source_impossible a
  222. 0222specialize gauss_mixed_sign_scaled_source_impossible x
  223. 0223specialize gauss_mixed_sign_scaled_source_impossible x3
  224. 0224specialize gauss_mixed_sign_scaled_source_impossible m
  225. 0225apply gauss_mixed_sign_scaled_source_impossible
  226. 0226exact hpodd
  227. 0227exact hp
  228. 0228exact hnotdiv
  229. 0229exact hsum_bound
  230. 0230exact hsum_nonzero
  231. 0231exact hisigned_left_right
  232. 0232exact hjsigned_right_right
  233. 0233cases hisigned_right
  234. 0234cases hjsigned
  235. 0235cases hjsigned_left
  236. 0236exfalso
  237. 0237specialize gauss_mixed_sign_scaled_source_impossible p
  238. 0238specialize gauss_mixed_sign_scaled_source_impossible h
  239. 0239specialize gauss_mixed_sign_scaled_source_impossible a
  240. 0240specialize gauss_mixed_sign_scaled_source_impossible x3
  241. 0241specialize gauss_mixed_sign_scaled_source_impossible x
  242. 0242specialize gauss_mixed_sign_scaled_source_impossible m
  243. 0243apply gauss_mixed_sign_scaled_source_impossible
  244. 0244exact hpodd
  245. 0245exact hp
  246. 0246exact hnotdiv
  247. 0247exact hreverse_sum_bound
  248. 0248exact hreverse_sum_nonzero
  249. 0249exact hjsigned_left_right
  250. 0250exact hisigned_right_right
  251. 0251cases hjsigned_right
  252. 0252specialize gauss_same_sign_scaled_source_unique p
  253. 0253specialize gauss_same_sign_scaled_source_unique h
  254. 0254specialize gauss_same_sign_scaled_source_unique a
  255. 0255specialize gauss_same_sign_scaled_source_unique x
  256. 0256specialize gauss_same_sign_scaled_source_unique x3
  257. 0257specialize gauss_same_sign_scaled_source_unique m
  258. 0258apply gauss_same_sign_scaled_source_unique
  259. 0259exact hp
  260. 0260exact hnotdiv
  261. 0261exact hxbounds_right
  262. 0262exact hybounds_right
  263. 0263right
  264. 0264split
  265. 0265exact hisigned_right_right
  266. 0266exact hjsigned_right_right
  267. 0267specialize beta_range_injective b
  268. 0268specialize beta_range_injective c
  269. 0269specialize beta_range_injective 1
  270. 0270specialize beta_range_injective h
  271. 0271specialize beta_range_injective i
  272. 0272specialize beta_range_injective j
  273. 0273specialize beta_range_injective x
  274. 0274specialize beta_range_injective x3
  275. 0275apply beta_range_injective
  276. 0276exact hrange
  277. 0277exact hi
  278. 0278exact hj
  279. 0279exact hentryi_witness_witness_witness_left
  280. 0280exact hentryj_witness_witness_witness_left
  281. 0281exact hsourceeq