BT00S0

prime_power_quotient_prefix_exists

Alpha body-checked · checked-use disabled

Every prime-power quotient prefix has a finite beta code.

Exact expanded PA statement

forall p n l. ((~(p = 1) /\ forall frm_prime_left_bls_prime frm_prime_right_bls_prime. p = frm_prime_left_bls_prime * frm_prime_right_bls_prime -> frm_prime_left_bls_prime = 1 \/ frm_prime_right_bls_prime = 1)) -> exists b c. (forall bls_index_bls_exists. (exists bls_gap_bls_exists_bound. bls_gap_bls_exists_bound + S (bls_index_bls_exists) = (l)) -> exists bls_power_bls_exists bls_quotient_bls_exists bls_remainder_bls_exists. ((exists bpvi_b_bls_bls_exists_power bpvi_c_bls_bls_exists_power. ((forall bpvi_i_bls_bls_exists_power. (exists bpvi_repeat_gap_bls_bls_exists_power. bpvi_repeat_gap_bls_bls_exists_power + S bpvi_i_bls_bls_exists_power = S bls_index_bls_exists) -> (((exists bpvi_h_bls_bls_exists_power_repeat. bpvi_h_bls_bls_exists_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_repeat. bpvi_b_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_repeat * S ((S (bpvi_i_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power) + (p)))) /\ (exists bpvi_u_bls_bls_exists_power bpvi_v_bls_bls_exists_power. ((((exists bpvi_h_bls_bls_exists_power_start. bpvi_h_bls_bls_exists_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_start. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_start * S ((S (0)) * bpvi_v_bls_bls_exists_power) + (1))) /\ ((((exists bpvi_h_bls_bls_exists_power_terminal. bpvi_h_bls_bls_exists_power_terminal + S (bls_power_bls_exists) = S ((S (S bls_index_bls_exists)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_terminal. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_terminal * S ((S (S bls_index_bls_exists)) * bpvi_v_bls_bls_exists_power) + (bls_power_bls_exists))) /\ forall bpvi_j_bls_bls_exists_power. (exists bpvi_product_gap_bls_bls_exists_power. bpvi_product_gap_bls_bls_exists_power + S bpvi_j_bls_bls_exists_power = S bls_index_bls_exists) -> exists bpvi_factor_bls_bls_exists_power bpvi_partial_bls_bls_exists_power bpvi_successor_bls_bls_exists_power. ((((exists bpvi_h_bls_bls_exists_power_factor. bpvi_h_bls_bls_exists_power_factor + S (bpvi_factor_bls_bls_exists_power) = S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_factor. bpvi_b_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_factor * S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power) + (bpvi_factor_bls_bls_exists_power))) /\ ((((exists bpvi_h_bls_bls_exists_power_partial. bpvi_h_bls_bls_exists_power_partial + S (bpvi_partial_bls_bls_exists_power) = S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_partial. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_partial * S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power) + (bpvi_partial_bls_bls_exists_power))) /\ ((((exists bpvi_h_bls_bls_exists_power_successor. bpvi_h_bls_bls_exists_power_successor + S (bpvi_successor_bls_bls_exists_power) = S ((S (S bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_successor. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_successor * S ((S (S bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power) + (bpvi_successor_bls_bls_exists_power))) /\ bpvi_successor_bls_bls_exists_power = bpvi_partial_bls_bls_exists_power * bpvi_factor_bls_bls_exists_power)))))))) /\ ((((exists ff_h_bls_bls_exists_quotient_entry. ff_h_bls_bls_exists_quotient_entry + S (bls_quotient_bls_exists) = S ((S (bls_index_bls_exists)) * c)) /\ exists ff_q_bls_bls_exists_quotient_entry. b = ff_q_bls_bls_exists_quotient_entry * S ((S (bls_index_bls_exists)) * c) + (bls_quotient_bls_exists))) /\ ((n = bls_power_bls_exists * bls_quotient_bls_exists + bls_remainder_bls_exists /\ exists bls_remainder_gap_bls_exists_division. bls_remainder_gap_bls_exists_division + S (bls_remainder_bls_exists) = bls_power_bls_exists)))))

Structural proof guide

Every prime-power quotient prefix has a finite beta code.

Direct prerequisites: add_eq_zero_right, succ_ne_zero, pow_exists, prime_nonzero, one_le_of_ne_zero, pow_nonzero_of_one_le, division_remainder_exists, beta_prefix_extend, finite_lt_succ_eq_or_lt. The authored body proceeds by structural induction (1), case analysis (15), intermediate claims (10), equality transport (6).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT000C succ_ne_zero BT0080 pow_exists BT003G prime_nonzero BT0010 one_le_of_ne_zero BT00Q1 pow_nonzero_of_one_le BT001P division_remainder_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct dependents

BT00S2 prime_legendre_sum_exists BT00ST legendre_sum_zero_extended_prefix BT00XR legendre_sum_extended_prefix_exists

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro n
  3. 0003induction l
  4. 0004intro hp
  5. 0005exists 0
  6. 0006exists 0
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010cases hi
  11. 0011have hsi : S i = 0
  12. 0012specialize add_eq_zero_right x
  13. 0013specialize add_eq_zero_right (S i)
  14. 0014apply add_eq_zero_right
  15. 0015exact hi_witness
  16. 0016specialize succ_ne_zero i
  17. 0017apply succ_ne_zero
  18. 0018exact hsi
  19. 0019intro hp
  20. 0020have hprevious : exists b c. (forall bls_index_bls_exists_previous. (exists bls_gap_bls_exists_previous_bound. bls_gap_bls_exists_previous_bound + S (bls_index_bls_exists_previous) = (l)) -> exists bls_power_bls_exists_previous bls_quotient_bls_exists_previous bls_remainder_bls_exists_previous. ((exists bpvi_b_bls_bls_exists_previous_power bpvi_c_bls_bls_exists_previous_power. ((forall bpvi_i_bls_bls_exists_previous_power. (exists bpvi_repeat_gap_bls_bls_exists_previous_power. bpvi_repeat_gap_bls_bls_exists_previous_power + S bpvi_i_bls_bls_exists_previous_power = S bls_index_bls_exists_previous) -> (((exists bpvi_h_bls_bls_exists_previous_power_repeat. bpvi_h_bls_bls_exists_previous_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_repeat. bpvi_b_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_repeat * S ((S (bpvi_i_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power) + (p)))) /\ (exists bpvi_u_bls_bls_exists_previous_power bpvi_v_bls_bls_exists_previous_power. ((((exists bpvi_h_bls_bls_exists_previous_power_start. bpvi_h_bls_bls_exists_previous_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_start. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_start * S ((S (0)) * bpvi_v_bls_bls_exists_previous_power) + (1))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_terminal. bpvi_h_bls_bls_exists_previous_power_terminal + S (bls_power_bls_exists_previous) = S ((S (S bls_index_bls_exists_previous)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_terminal. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_terminal * S ((S (S bls_index_bls_exists_previous)) * bpvi_v_bls_bls_exists_previous_power) + (bls_power_bls_exists_previous))) /\ forall bpvi_j_bls_bls_exists_previous_power. (exists bpvi_product_gap_bls_bls_exists_previous_power. bpvi_product_gap_bls_bls_exists_previous_power + S bpvi_j_bls_bls_exists_previous_power = S bls_index_bls_exists_previous) -> exists bpvi_factor_bls_bls_exists_previous_power bpvi_partial_bls_bls_exists_previous_power bpvi_successor_bls_bls_exists_previous_power. ((((exists bpvi_h_bls_bls_exists_previous_power_factor. bpvi_h_bls_bls_exists_previous_power_factor + S (bpvi_factor_bls_bls_exists_previous_power) = S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_factor. bpvi_b_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_factor * S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power) + (bpvi_factor_bls_bls_exists_previous_power))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_partial. bpvi_h_bls_bls_exists_previous_power_partial + S (bpvi_partial_bls_bls_exists_previous_power) = S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_partial. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_partial * S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power) + (bpvi_partial_bls_bls_exists_previous_power))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_successor. bpvi_h_bls_bls_exists_previous_power_successor + S (bpvi_successor_bls_bls_exists_previous_power) = S ((S (S bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_successor. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_successor * S ((S (S bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power) + (bpvi_successor_bls_bls_exists_previous_power))) /\ bpvi_successor_bls_bls_exists_previous_power = bpvi_partial_bls_bls_exists_previous_power * bpvi_factor_bls_bls_exists_previous_power)))))))) /\ ((((exists ff_h_bls_bls_exists_previous_quotient_entry. ff_h_bls_bls_exists_previous_quotient_entry + S (bls_quotient_bls_exists_previous) = S ((S (bls_index_bls_exists_previous)) * c)) /\ exists ff_q_bls_bls_exists_previous_quotient_entry. b = ff_q_bls_bls_exists_previous_quotient_entry * S ((S (bls_index_bls_exists_previous)) * c) + (bls_quotient_bls_exists_previous))) /\ ((n = bls_power_bls_exists_previous * bls_quotient_bls_exists_previous + bls_remainder_bls_exists_previous /\ exists bls_remainder_gap_bls_exists_previous_division. bls_remainder_gap_bls_exists_previous_division + S (bls_remainder_bls_exists_previous) = bls_power_bls_exists_previous)))))
  21. 0021apply IH
  22. 0022exact hp
  23. 0023cases hprevious
  24. 0024cases hprevious_witness
  25. 0025have hpower : exists D. (exists bpvi_b_bls_exists_last_power bpvi_c_bls_exists_last_power. ((forall bpvi_i_bls_exists_last_power. (exists bpvi_repeat_gap_bls_exists_last_power. bpvi_repeat_gap_bls_exists_last_power + S bpvi_i_bls_exists_last_power = S l) -> (((exists bpvi_h_bls_exists_last_power_repeat. bpvi_h_bls_exists_last_power_repeat + S (p) = S ((S (bpvi_i_bls_exists_last_power)) * bpvi_c_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_repeat. bpvi_b_bls_exists_last_power = bpvi_q_bls_exists_last_power_repeat * S ((S (bpvi_i_bls_exists_last_power)) * bpvi_c_bls_exists_last_power) + (p)))) /\ (exists bpvi_u_bls_exists_last_power bpvi_v_bls_exists_last_power. ((((exists bpvi_h_bls_exists_last_power_start. bpvi_h_bls_exists_last_power_start + S (1) = S ((S (0)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_start. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_start * S ((S (0)) * bpvi_v_bls_exists_last_power) + (1))) /\ ((((exists bpvi_h_bls_exists_last_power_terminal. bpvi_h_bls_exists_last_power_terminal + S (D) = S ((S (S l)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_terminal. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_terminal * S ((S (S l)) * bpvi_v_bls_exists_last_power) + (D))) /\ forall bpvi_j_bls_exists_last_power. (exists bpvi_product_gap_bls_exists_last_power. bpvi_product_gap_bls_exists_last_power + S bpvi_j_bls_exists_last_power = S l) -> exists bpvi_factor_bls_exists_last_power bpvi_partial_bls_exists_last_power bpvi_successor_bls_exists_last_power. ((((exists bpvi_h_bls_exists_last_power_factor. bpvi_h_bls_exists_last_power_factor + S (bpvi_factor_bls_exists_last_power) = S ((S (bpvi_j_bls_exists_last_power)) * bpvi_c_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_factor. bpvi_b_bls_exists_last_power = bpvi_q_bls_exists_last_power_factor * S ((S (bpvi_j_bls_exists_last_power)) * bpvi_c_bls_exists_last_power) + (bpvi_factor_bls_exists_last_power))) /\ ((((exists bpvi_h_bls_exists_last_power_partial. bpvi_h_bls_exists_last_power_partial + S (bpvi_partial_bls_exists_last_power) = S ((S (bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_partial. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_partial * S ((S (bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power) + (bpvi_partial_bls_exists_last_power))) /\ ((((exists bpvi_h_bls_exists_last_power_successor. bpvi_h_bls_exists_last_power_successor + S (bpvi_successor_bls_exists_last_power) = S ((S (S bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_successor. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_successor * S ((S (S bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power) + (bpvi_successor_bls_exists_last_power))) /\ bpvi_successor_bls_exists_last_power = bpvi_partial_bls_exists_last_power * bpvi_factor_bls_exists_last_power))))))))
  26. 0026specialize pow_exists p
  27. 0027specialize pow_exists (S l)
  28. 0028exact pow_exists
  29. 0029cases hpower
  30. 0030have hp0 : ~(p = 0)
  31. 0031intro hpzero
  32. 0032specialize prime_nonzero p
  33. 0033apply prime_nonzero
  34. 0034exact hp
  35. 0035exact hpzero
  36. 0036have hp1 : exists k. k + 1 = p
  37. 0037specialize one_le_of_ne_zero p
  38. 0038apply one_le_of_ne_zero
  39. 0039exact hp0
  40. 0040have hD0 : ~(x2 = 0)
  41. 0041intro hzero
  42. 0042specialize pow_nonzero_of_one_le p
  43. 0043specialize pow_nonzero_of_one_le (S l)
  44. 0044specialize pow_nonzero_of_one_le x2
  45. 0045apply pow_nonzero_of_one_le
  46. 0046exact hp1
  47. 0047exact hpower_witness
  48. 0048exact hzero
  49. 0049have hdivision : exists q r. ((n = x2 * q + r /\ exists bls_remainder_gap_bls_exists_division_witness. bls_remainder_gap_bls_exists_division_witness + S (r) = x2))
  50. 0050specialize division_remainder_exists x2
  51. 0051specialize division_remainder_exists n
  52. 0052apply division_remainder_exists
  53. 0053exact hD0
  54. 0054cases hdivision
  55. 0055cases hdivision_witness
  56. 0056have hextension : exists z d. ((((exists ff_h_bls_exists_extension_last. ff_h_bls_exists_extension_last + S (x3) = S ((S (l)) * d)) /\ exists ff_q_bls_exists_extension_last. z = ff_q_bls_exists_extension_last * S ((S (l)) * d) + (x3))) /\ forall i a. (exists h. h + S i = l) -> (((exists ff_h_bls_exists_extension_old. ff_h_bls_exists_extension_old + S (a) = S ((S (i)) * x1)) /\ exists ff_q_bls_exists_extension_old. x = ff_q_bls_exists_extension_old * S ((S (i)) * x1) + (a))) -> (((exists ff_h_bls_exists_extension_new. ff_h_bls_exists_extension_new + S (a) = S ((S (i)) * d)) /\ exists ff_q_bls_exists_extension_new. z = ff_q_bls_exists_extension_new * S ((S (i)) * d) + (a))))
  57. 0057specialize beta_prefix_extend l
  58. 0058specialize beta_prefix_extend x
  59. 0059specialize beta_prefix_extend x1
  60. 0060specialize beta_prefix_extend x3
  61. 0061exact beta_prefix_extend
  62. 0062cases hextension
  63. 0063cases hextension_witness
  64. 0064cases hextension_witness_witness
  65. 0065exists x5
  66. 0066exists x6
  67. 0067intro i
  68. 0068intro hi
  69. 0069have hsplit : i = l \/ exists gap. gap + S i = l
  70. 0070specialize finite_lt_succ_eq_or_lt l
  71. 0071specialize finite_lt_succ_eq_or_lt i
  72. 0072apply finite_lt_succ_eq_or_lt
  73. 0073exact hi
  74. 0074cases hsplit
  75. 0075exists x2
  76. 0076exists x3
  77. 0077exists x4
  78. 0078rewrite hsplit_left
  79. 0079rewrite hsplit_left
  80. 0080rewrite hsplit_left
  81. 0081rewrite hsplit_left
  82. 0082rewrite hsplit_left
  83. 0083rewrite hsplit_left
  84. 0084split
  85. 0085exact hpower_witness
  86. 0086split
  87. 0087exact hextension_witness_witness_left
  88. 0088exact hdivision_witness_witness
  89. 0089have hold : exists D q r. ((exists bpvi_b_bls_exists_old_power bpvi_c_bls_exists_old_power. ((forall bpvi_i_bls_exists_old_power. (exists bpvi_repeat_gap_bls_exists_old_power. bpvi_repeat_gap_bls_exists_old_power + S bpvi_i_bls_exists_old_power = S i) -> (((exists bpvi_h_bls_exists_old_power_repeat. bpvi_h_bls_exists_old_power_repeat + S (p) = S ((S (bpvi_i_bls_exists_old_power)) * bpvi_c_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_repeat. bpvi_b_bls_exists_old_power = bpvi_q_bls_exists_old_power_repeat * S ((S (bpvi_i_bls_exists_old_power)) * bpvi_c_bls_exists_old_power) + (p)))) /\ (exists bpvi_u_bls_exists_old_power bpvi_v_bls_exists_old_power. ((((exists bpvi_h_bls_exists_old_power_start. bpvi_h_bls_exists_old_power_start + S (1) = S ((S (0)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_start. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_start * S ((S (0)) * bpvi_v_bls_exists_old_power) + (1))) /\ ((((exists bpvi_h_bls_exists_old_power_terminal. bpvi_h_bls_exists_old_power_terminal + S (D) = S ((S (S i)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_terminal. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_terminal * S ((S (S i)) * bpvi_v_bls_exists_old_power) + (D))) /\ forall bpvi_j_bls_exists_old_power. (exists bpvi_product_gap_bls_exists_old_power. bpvi_product_gap_bls_exists_old_power + S bpvi_j_bls_exists_old_power = S i) -> exists bpvi_factor_bls_exists_old_power bpvi_partial_bls_exists_old_power bpvi_successor_bls_exists_old_power. ((((exists bpvi_h_bls_exists_old_power_factor. bpvi_h_bls_exists_old_power_factor + S (bpvi_factor_bls_exists_old_power) = S ((S (bpvi_j_bls_exists_old_power)) * bpvi_c_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_factor. bpvi_b_bls_exists_old_power = bpvi_q_bls_exists_old_power_factor * S ((S (bpvi_j_bls_exists_old_power)) * bpvi_c_bls_exists_old_power) + (bpvi_factor_bls_exists_old_power))) /\ ((((exists bpvi_h_bls_exists_old_power_partial. bpvi_h_bls_exists_old_power_partial + S (bpvi_partial_bls_exists_old_power) = S ((S (bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_partial. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_partial * S ((S (bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power) + (bpvi_partial_bls_exists_old_power))) /\ ((((exists bpvi_h_bls_exists_old_power_successor. bpvi_h_bls_exists_old_power_successor + S (bpvi_successor_bls_exists_old_power) = S ((S (S bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_successor. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_successor * S ((S (S bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power) + (bpvi_successor_bls_exists_old_power))) /\ bpvi_successor_bls_exists_old_power = bpvi_partial_bls_exists_old_power * bpvi_factor_bls_exists_old_power)))))))) /\ ((((exists ff_h_bls_exists_old_entry. ff_h_bls_exists_old_entry + S (q) = S ((S (i)) * x1)) /\ exists ff_q_bls_exists_old_entry. x = ff_q_bls_exists_old_entry * S ((S (i)) * x1) + (q))) /\ ((n = D * q + r /\ exists bls_remainder_gap_bls_exists_old_division. bls_remainder_gap_bls_exists_old_division + S (r) = D))))
  90. 0090specialize hprevious_witness_witness i
  91. 0091apply hprevious_witness_witness
  92. 0092exact hsplit_right
  93. 0093cases hold
  94. 0094cases hold_witness
  95. 0095cases hold_witness_witness
  96. 0096cases hold_witness_witness_witness
  97. 0097cases hold_witness_witness_witness_right
  98. 0098exists x7
  99. 0099exists x8
  100. 0100exists x9
  101. 0101split
  102. 0102exact hold_witness_witness_witness_left
  103. 0103split
  104. 0104specialize hextension_witness_witness_right i
  105. 0105specialize hextension_witness_witness_right x8
  106. 0106apply hextension_witness_witness_right
  107. 0107exact hsplit_right
  108. 0108exact hold_witness_witness_witness_right_left
  109. 0109exact hold_witness_witness_witness_right_right