Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Exact expanded PA statement
forall p a B. exists e. (((exists bpv_gap_bounded_exponent_bound. bpv_gap_bounded_exponent_bound + e = B) /\ (exists bpv_result_bounded_selected. ((exists ff_b_bounded_selected_power ff_c_bounded_selected_power. ((forall ff_i_bounded_selected_power_repeat. (exists ff_lt_bounded_selected_power_repeat_bound. ff_lt_bounded_selected_power_repeat_bound + S ff_i_bounded_selected_power_repeat = e) -> (((exists ff_h_bounded_selected_power_repeat_decoded. ff_h_bounded_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bounded_selected_power_repeat)) * ff_c_bounded_selected_power)) /\ exists ff_q_bounded_selected_power_repeat_decoded. ff_b_bounded_selected_power = ff_q_bounded_selected_power_repeat_decoded * S ((S (ff_i_bounded_selected_power_repeat)) * ff_c_bounded_selected_power) + (p)))) /\ (exists ff_u_bounded_selected_power_product ff_v_bounded_selected_power_product. ((((exists ff_h_bounded_selected_power_product_start. ff_h_bounded_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bounded_selected_power_product)) /\ exists ff_q_bounded_selected_power_product_start. ff_u_bounded_selected_power_product = ff_q_bounded_selected_power_product_start * S ((S (0)) * ff_v_bounded_selected_power_product) + (1))) /\ ((((exists ff_h_bounded_selected_power_product_terminal. ff_h_bounded_selected_power_product_terminal + S (bpv_result_bounded_selected) = S ((S (e)) * ff_v_bounded_selected_power_product)) /\ exists ff_q_bounded_selected_power_product_terminal. ff_u_bounded_selected_power_product = ff_q_bounded_selected_power_product_terminal * S ((S (e)) * ff_v_bounded_selected_power_product) + (bpv_result_bounded_selected))) /\ forall ff_i_bounded_selected_power_product. (exists ff_lt_bounded_selected_power_product_bound. ff_lt_bounded_selected_power_product_bound + S ff_i_bounded_selected_power_product = e) -> exists ff_p_bounded_selected_power_product ff_r_bounded_selected_power_product ff_s_bounded_selected_power_product. ((((exists ff_h_bounded_selected_power_product_factor. ff_h_bounded_selected_power_product_factor + S (ff_p_bounded_selected_power_product) = S ((S (ff_i_bounded_selected_power_product)) * ff_c_bounded_selected_power)) /\ exists ff_q_bounded_selected_power_product_factor. ff_b_bounded_selected_power = ff_q_bounded_selected_power_product_factor * S ((S (ff_i_bounded_selected_power_product)) * ff_c_bounded_selected_power) + (ff_p_bounded_selected_power_product))) /\ ((((exists ff_h_bounded_selected_power_product_partial. ff_h_bounded_selected_power_product_partial + S (ff_r_bounded_selected_power_product) = S ((S (ff_i_bounded_selected_power_product)) * ff_v_bounded_selected_power_product)) /\ exists ff_q_bounded_selected_power_product_partial. ff_u_bounded_selected_power_product = ff_q_bounded_selected_power_product_partial * S ((S (ff_i_bounded_selected_power_product)) * ff_v_bounded_selected_power_product) + (ff_r_bounded_selected_power_product))) /\ ((((exists ff_h_bounded_selected_power_product_successor. ff_h_bounded_selected_power_product_successor + S (ff_s_bounded_selected_power_product) = S ((S (S ff_i_bounded_selected_power_product)) * ff_v_bounded_selected_power_product)) /\ exists ff_q_bounded_selected_power_product_successor. ff_u_bounded_selected_power_product = ff_q_bounded_selected_power_product_successor * S ((S (S ff_i_bounded_selected_power_product)) * ff_v_bounded_selected_power_product) + (ff_s_bounded_selected_power_product))) /\ ff_s_bounded_selected_power_product = ff_r_bounded_selected_power_product * ff_p_bounded_selected_power_product)))))))) /\ (exists bpv_factor_bounded_selected_divides. a = bpv_result_bounded_selected * bpv_factor_bounded_selected_divides)))) /\ forall bpv_candidate_bounded. (exists bpv_gap_bounded_candidate_bound. bpv_gap_bounded_candidate_bound + bpv_candidate_bounded = B) -> (exists bpv_result_bounded_candidate. ((exists ff_b_bounded_candidate_power ff_c_bounded_candidate_power. ((forall ff_i_bounded_candidate_power_repeat. (exists ff_lt_bounded_candidate_power_repeat_bound. ff_lt_bounded_candidate_power_repeat_bound + S ff_i_bounded_candidate_power_repeat = bpv_candidate_bounded) -> (((exists ff_h_bounded_candidate_power_repeat_decoded. ff_h_bounded_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bounded_candidate_power_repeat)) * ff_c_bounded_candidate_power)) /\ exists ff_q_bounded_candidate_power_repeat_decoded. ff_b_bounded_candidate_power = ff_q_bounded_candidate_power_repeat_decoded * S ((S (ff_i_bounded_candidate_power_repeat)) * ff_c_bounded_candidate_power) + (p)))) /\ (exists ff_u_bounded_candidate_power_product ff_v_bounded_candidate_power_product. ((((exists ff_h_bounded_candidate_power_product_start. ff_h_bounded_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bounded_candidate_power_product)) /\ exists ff_q_bounded_candidate_power_product_start. ff_u_bounded_candidate_power_product = ff_q_bounded_candidate_power_product_start * S ((S (0)) * ff_v_bounded_candidate_power_product) + (1))) /\ ((((exists ff_h_bounded_candidate_power_product_terminal. ff_h_bounded_candidate_power_product_terminal + S (bpv_result_bounded_candidate) = S ((S (bpv_candidate_bounded)) * ff_v_bounded_candidate_power_product)) /\ exists ff_q_bounded_candidate_power_product_terminal. ff_u_bounded_candidate_power_product = ff_q_bounded_candidate_power_product_terminal * S ((S (bpv_candidate_bounded)) * ff_v_bounded_candidate_power_product) + (bpv_result_bounded_candidate))) /\ forall ff_i_bounded_candidate_power_product. (exists ff_lt_bounded_candidate_power_product_bound. ff_lt_bounded_candidate_power_product_bound + S ff_i_bounded_candidate_power_product = bpv_candidate_bounded) -> exists ff_p_bounded_candidate_power_product ff_r_bounded_candidate_power_product ff_s_bounded_candidate_power_product. ((((exists ff_h_bounded_candidate_power_product_factor. ff_h_bounded_candidate_power_product_factor + S (ff_p_bounded_candidate_power_product) = S ((S (ff_i_bounded_candidate_power_product)) * ff_c_bounded_candidate_power)) /\ exists ff_q_bounded_candidate_power_product_factor. ff_b_bounded_candidate_power = ff_q_bounded_candidate_power_product_factor * S ((S (ff_i_bounded_candidate_power_product)) * ff_c_bounded_candidate_power) + (ff_p_bounded_candidate_power_product))) /\ ((((exists ff_h_bounded_candidate_power_product_partial. ff_h_bounded_candidate_power_product_partial + S (ff_r_bounded_candidate_power_product) = S ((S (ff_i_bounded_candidate_power_product)) * ff_v_bounded_candidate_power_product)) /\ exists ff_q_bounded_candidate_power_product_partial. ff_u_bounded_candidate_power_product = ff_q_bounded_candidate_power_product_partial * S ((S (ff_i_bounded_candidate_power_product)) * ff_v_bounded_candidate_power_product) + (ff_r_bounded_candidate_power_product))) /\ ((((exists ff_h_bounded_candidate_power_product_successor. ff_h_bounded_candidate_power_product_successor + S (ff_s_bounded_candidate_power_product) = S ((S (S ff_i_bounded_candidate_power_product)) * ff_v_bounded_candidate_power_product)) /\ exists ff_q_bounded_candidate_power_product_successor. ff_u_bounded_candidate_power_product = ff_q_bounded_candidate_power_product_successor * S ((S (S ff_i_bounded_candidate_power_product)) * ff_v_bounded_candidate_power_product) + (ff_s_bounded_candidate_power_product))) /\ ff_s_bounded_candidate_power_product = ff_r_bounded_candidate_power_product * ff_p_bounded_candidate_power_product)))))))) /\ (exists bpv_factor_bounded_candidate_divides. a = bpv_result_bounded_candidate * bpv_factor_bounded_candidate_divides))) -> (exists bpv_gap_bounded_maximal. bpv_gap_bounded_maximal + bpv_candidate_bounded = e))Structural proof guide
Every explicit exponent bound has a greatest power-divisor exponent.
Direct prerequisites: bounded_power_valuation_search, power_divides_zero, zero_le. The authored body proceeds by case analysis (2), intermediate claims (2).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (3)
01Fix variables and assumptionsL1–3
02Establish hsearchL4–8
Establish this local claim before using it. It is not an additional assumption.
- L4
have hsearch : (∀ x. Le(x,B) → ¬PowerDivides(p,x,a)) ∨ (∃ x. BoundedPowerValuation(p,a,B,x))Definitions: LePowerDividesBoundedPowerValuation - L5
specialize bounded_power_valuation_search B - L6
specialize bounded_power_valuation_search p - L7
specialize bounded_power_valuation_search a - L8
exact bounded_power_valuation_search
03Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
cases hsearch
04Establish hzeroL10–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power divides zero.
05Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
exfalso
06Use earlier factsL18–21
07Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
cases hsearch_right
08Construct an explicit witnessL23–23
Supply the displayed value, then prove that it has the required property.
- L23
exists x
09Use earlier factsL24–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L24
exact hsearch_right_witness
Original exact command ledger · 24 lines
- 0001
intro p - 0002
intro a - 0003
intro B - 0004
have hsearch : (forall f. (exists bpv_gap_search_none_bound. bpv_gap_search_none_bound + f = B) -> ~(exists bpv_result_search_property. ((exists ff_b_search_property_power ff_c_search_property_power. ((forall ff_i_search_property_power_repeat. (exists ff_lt_search_property_power_repeat_bound. ff_lt_search_property_power_repeat_bound + S ff_i_search_property_power_repeat = f) -> (((exists ff_h_search_property_power_repeat_decoded. ff_h_search_property_power_repeat_decoded + S (p) = S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_repeat_decoded. ff_b_search_property_power = ff_q_search_property_power_repeat_decoded * S ((S (ff_i_search_property_power_repeat)) * ff_c_search_property_power) + (p)))) /\ (exists ff_u_search_property_power_product ff_v_search_property_power_product. ((((exists ff_h_search_property_power_product_start. ff_h_search_property_power_product_start + S (1) = S ((S (0)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_start. ff_u_search_property_power_product = ff_q_search_property_power_product_start * S ((S (0)) * ff_v_search_property_power_product) + (1))) /\ ((((exists ff_h_search_property_power_product_terminal. ff_h_search_property_power_product_terminal + S (bpv_result_search_property) = S ((S (f)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_terminal. ff_u_search_property_power_product = ff_q_search_property_power_product_terminal * S ((S (f)) * ff_v_search_property_power_product) + (bpv_result_search_property))) /\ forall ff_i_search_property_power_product. (exists ff_lt_search_property_power_product_bound. ff_lt_search_property_power_product_bound + S ff_i_search_property_power_product = f) -> exists ff_p_search_property_power_product ff_r_search_property_power_product ff_s_search_property_power_product. ((((exists ff_h_search_property_power_product_factor. ff_h_search_property_power_product_factor + S (ff_p_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power)) /\ exists ff_q_search_property_power_product_factor. ff_b_search_property_power = ff_q_search_property_power_product_factor * S ((S (ff_i_search_property_power_product)) * ff_c_search_property_power) + (ff_p_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_partial. ff_h_search_property_power_product_partial + S (ff_r_search_property_power_product) = S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_partial. ff_u_search_property_power_product = ff_q_search_property_power_product_partial * S ((S (ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_r_search_property_power_product))) /\ ((((exists ff_h_search_property_power_product_successor. ff_h_search_property_power_product_successor + S (ff_s_search_property_power_product) = S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product)) /\ exists ff_q_search_property_power_product_successor. ff_u_search_property_power_product = ff_q_search_property_power_product_successor * S ((S (S ff_i_search_property_power_product)) * ff_v_search_property_power_product) + (ff_s_search_property_power_product))) /\ ff_s_search_property_power_product = ff_r_search_property_power_product * ff_p_search_property_power_product)))))))) /\ (exists bpv_factor_search_property_divides. a = bpv_result_search_property * bpv_factor_search_property_divides)))) \/ (exists e. ((exists bpv_gap_search_selected_bound. bpv_gap_search_selected_bound + e = B) /\ (exists bpv_result_search_selected. ((exists ff_b_search_selected_power ff_c_search_selected_power. ((forall ff_i_search_selected_power_repeat. (exists ff_lt_search_selected_power_repeat_bound. ff_lt_search_selected_power_repeat_bound + S ff_i_search_selected_power_repeat = e) -> (((exists ff_h_search_selected_power_repeat_decoded. ff_h_search_selected_power_repeat_decoded + S (p) = S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_repeat_decoded. ff_b_search_selected_power = ff_q_search_selected_power_repeat_decoded * S ((S (ff_i_search_selected_power_repeat)) * ff_c_search_selected_power) + (p)))) /\ (exists ff_u_search_selected_power_product ff_v_search_selected_power_product. ((((exists ff_h_search_selected_power_product_start. ff_h_search_selected_power_product_start + S (1) = S ((S (0)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_start. ff_u_search_selected_power_product = ff_q_search_selected_power_product_start * S ((S (0)) * ff_v_search_selected_power_product) + (1))) /\ ((((exists ff_h_search_selected_power_product_terminal. ff_h_search_selected_power_product_terminal + S (bpv_result_search_selected) = S ((S (e)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_terminal. ff_u_search_selected_power_product = ff_q_search_selected_power_product_terminal * S ((S (e)) * ff_v_search_selected_power_product) + (bpv_result_search_selected))) /\ forall ff_i_search_selected_power_product. (exists ff_lt_search_selected_power_product_bound. ff_lt_search_selected_power_product_bound + S ff_i_search_selected_power_product = e) -> exists ff_p_search_selected_power_product ff_r_search_selected_power_product ff_s_search_selected_power_product. ((((exists ff_h_search_selected_power_product_factor. ff_h_search_selected_power_product_factor + S (ff_p_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power)) /\ exists ff_q_search_selected_power_product_factor. ff_b_search_selected_power = ff_q_search_selected_power_product_factor * S ((S (ff_i_search_selected_power_product)) * ff_c_search_selected_power) + (ff_p_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_partial. ff_h_search_selected_power_product_partial + S (ff_r_search_selected_power_product) = S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_partial. ff_u_search_selected_power_product = ff_q_search_selected_power_product_partial * S ((S (ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_r_search_selected_power_product))) /\ ((((exists ff_h_search_selected_power_product_successor. ff_h_search_selected_power_product_successor + S (ff_s_search_selected_power_product) = S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product)) /\ exists ff_q_search_selected_power_product_successor. ff_u_search_selected_power_product = ff_q_search_selected_power_product_successor * S ((S (S ff_i_search_selected_power_product)) * ff_v_search_selected_power_product) + (ff_s_search_selected_power_product))) /\ ff_s_search_selected_power_product = ff_r_search_selected_power_product * ff_p_search_selected_power_product)))))))) /\ (exists bpv_factor_search_selected_divides. a = bpv_result_search_selected * bpv_factor_search_selected_divides)))) /\ forall f. (exists bpv_gap_search_candidate_bound. bpv_gap_search_candidate_bound + f = B) -> (exists bpv_result_search_candidate. ((exists ff_b_search_candidate_power ff_c_search_candidate_power. ((forall ff_i_search_candidate_power_repeat. (exists ff_lt_search_candidate_power_repeat_bound. ff_lt_search_candidate_power_repeat_bound + S ff_i_search_candidate_power_repeat = f) -> (((exists ff_h_search_candidate_power_repeat_decoded. ff_h_search_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_repeat_decoded. ff_b_search_candidate_power = ff_q_search_candidate_power_repeat_decoded * S ((S (ff_i_search_candidate_power_repeat)) * ff_c_search_candidate_power) + (p)))) /\ (exists ff_u_search_candidate_power_product ff_v_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_start. ff_h_search_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_start. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_start * S ((S (0)) * ff_v_search_candidate_power_product) + (1))) /\ ((((exists ff_h_search_candidate_power_product_terminal. ff_h_search_candidate_power_product_terminal + S (bpv_result_search_candidate) = S ((S (f)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_terminal. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_terminal * S ((S (f)) * ff_v_search_candidate_power_product) + (bpv_result_search_candidate))) /\ forall ff_i_search_candidate_power_product. (exists ff_lt_search_candidate_power_product_bound. ff_lt_search_candidate_power_product_bound + S ff_i_search_candidate_power_product = f) -> exists ff_p_search_candidate_power_product ff_r_search_candidate_power_product ff_s_search_candidate_power_product. ((((exists ff_h_search_candidate_power_product_factor. ff_h_search_candidate_power_product_factor + S (ff_p_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power)) /\ exists ff_q_search_candidate_power_product_factor. ff_b_search_candidate_power = ff_q_search_candidate_power_product_factor * S ((S (ff_i_search_candidate_power_product)) * ff_c_search_candidate_power) + (ff_p_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_partial. ff_h_search_candidate_power_product_partial + S (ff_r_search_candidate_power_product) = S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_partial. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_partial * S ((S (ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_r_search_candidate_power_product))) /\ ((((exists ff_h_search_candidate_power_product_successor. ff_h_search_candidate_power_product_successor + S (ff_s_search_candidate_power_product) = S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product)) /\ exists ff_q_search_candidate_power_product_successor. ff_u_search_candidate_power_product = ff_q_search_candidate_power_product_successor * S ((S (S ff_i_search_candidate_power_product)) * ff_v_search_candidate_power_product) + (ff_s_search_candidate_power_product))) /\ ff_s_search_candidate_power_product = ff_r_search_candidate_power_product * ff_p_search_candidate_power_product)))))))) /\ (exists bpv_factor_search_candidate_divides. a = bpv_result_search_candidate * bpv_factor_search_candidate_divides))) -> (exists bpv_gap_search_maximal. bpv_gap_search_maximal + f = e)) - 0005
specialize bounded_power_valuation_search B - 0006
specialize bounded_power_valuation_search p - 0007
specialize bounded_power_valuation_search a - 0008
exact bounded_power_valuation_search - 0009
cases hsearch - 0010
have hzero : (exists bpvi_result_exists_zero. ((exists bpvi_b_exists_zero_power bpvi_c_exists_zero_power. ((forall bpvi_i_exists_zero_power. (exists bpvi_repeat_gap_exists_zero_power. bpvi_repeat_gap_exists_zero_power + S bpvi_i_exists_zero_power = 0) -> (((exists bpvi_h_exists_zero_power_repeat. bpvi_h_exists_zero_power_repeat + S (p) = S ((S (bpvi_i_exists_zero_power)) * bpvi_c_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_repeat. bpvi_b_exists_zero_power = bpvi_q_exists_zero_power_repeat * S ((S (bpvi_i_exists_zero_power)) * bpvi_c_exists_zero_power) + (p)))) /\ (exists bpvi_u_exists_zero_power bpvi_v_exists_zero_power. ((((exists bpvi_h_exists_zero_power_start. bpvi_h_exists_zero_power_start + S (1) = S ((S (0)) * bpvi_v_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_start. bpvi_u_exists_zero_power = bpvi_q_exists_zero_power_start * S ((S (0)) * bpvi_v_exists_zero_power) + (1))) /\ ((((exists bpvi_h_exists_zero_power_terminal. bpvi_h_exists_zero_power_terminal + S (bpvi_result_exists_zero) = S ((S (0)) * bpvi_v_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_terminal. bpvi_u_exists_zero_power = bpvi_q_exists_zero_power_terminal * S ((S (0)) * bpvi_v_exists_zero_power) + (bpvi_result_exists_zero))) /\ forall bpvi_j_exists_zero_power. (exists bpvi_product_gap_exists_zero_power. bpvi_product_gap_exists_zero_power + S bpvi_j_exists_zero_power = 0) -> exists bpvi_factor_exists_zero_power bpvi_partial_exists_zero_power bpvi_successor_exists_zero_power. ((((exists bpvi_h_exists_zero_power_factor. bpvi_h_exists_zero_power_factor + S (bpvi_factor_exists_zero_power) = S ((S (bpvi_j_exists_zero_power)) * bpvi_c_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_factor. bpvi_b_exists_zero_power = bpvi_q_exists_zero_power_factor * S ((S (bpvi_j_exists_zero_power)) * bpvi_c_exists_zero_power) + (bpvi_factor_exists_zero_power))) /\ ((((exists bpvi_h_exists_zero_power_partial. bpvi_h_exists_zero_power_partial + S (bpvi_partial_exists_zero_power) = S ((S (bpvi_j_exists_zero_power)) * bpvi_v_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_partial. bpvi_u_exists_zero_power = bpvi_q_exists_zero_power_partial * S ((S (bpvi_j_exists_zero_power)) * bpvi_v_exists_zero_power) + (bpvi_partial_exists_zero_power))) /\ ((((exists bpvi_h_exists_zero_power_successor. bpvi_h_exists_zero_power_successor + S (bpvi_successor_exists_zero_power) = S ((S (S bpvi_j_exists_zero_power)) * bpvi_v_exists_zero_power)) /\ exists bpvi_q_exists_zero_power_successor. bpvi_u_exists_zero_power = bpvi_q_exists_zero_power_successor * S ((S (S bpvi_j_exists_zero_power)) * bpvi_v_exists_zero_power) + (bpvi_successor_exists_zero_power))) /\ bpvi_successor_exists_zero_power = bpvi_partial_exists_zero_power * bpvi_factor_exists_zero_power)))))))) /\ exists bpvi_divisor_factor_exists_zero. a = bpvi_result_exists_zero * bpvi_divisor_factor_exists_zero)) - 0011
specialize power_divides_zero p - 0012
specialize power_divides_zero a - 0013
specialize power_divides_zero 0 - 0014
apply power_divides_zero - 0015
refl - 0016
specialize hsearch_left 0 - 0017
exfalso - 0018
apply hsearch_left - 0019
specialize zero_le B - 0020
exact zero_le - 0021
exact hzero - 0022
cases hsearch_right - 0023
exists x - 0024
exact hsearch_right_witness