BT00W0

power_valuation_nonzero_exponent_divides_base

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A nonzero valuation exponent exposes the base as a divisor.

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 c e. (((exists bpv_gap_bpvnedb_source_exponent_bound. bpv_gap_bpvnedb_source_exponent_bound + e = c) /\ (exists bpv_result_bpvnedb_source_selected. ((exists ff_b_bpvnedb_source_selected_power ff_c_bpvnedb_source_selected_power. ((forall ff_i_bpvnedb_source_selected_power_repeat. (exists ff_lt_bpvnedb_source_selected_power_repeat_bound. ff_lt_bpvnedb_source_selected_power_repeat_bound + S ff_i_bpvnedb_source_selected_power_repeat = e) -> (((exists ff_h_bpvnedb_source_selected_power_repeat_decoded. ff_h_bpvnedb_source_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bpvnedb_source_selected_power_repeat)) * ff_c_bpvnedb_source_selected_power)) /\ exists ff_q_bpvnedb_source_selected_power_repeat_decoded. ff_b_bpvnedb_source_selected_power = ff_q_bpvnedb_source_selected_power_repeat_decoded * S ((S (ff_i_bpvnedb_source_selected_power_repeat)) * ff_c_bpvnedb_source_selected_power) + (p)))) /\ (exists ff_u_bpvnedb_source_selected_power_product ff_v_bpvnedb_source_selected_power_product. ((((exists ff_h_bpvnedb_source_selected_power_product_start. ff_h_bpvnedb_source_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpvnedb_source_selected_power_product)) /\ exists ff_q_bpvnedb_source_selected_power_product_start. ff_u_bpvnedb_source_selected_power_product = ff_q_bpvnedb_source_selected_power_product_start * S ((S (0)) * ff_v_bpvnedb_source_selected_power_product) + (1))) /\ ((((exists ff_h_bpvnedb_source_selected_power_product_terminal. ff_h_bpvnedb_source_selected_power_product_terminal + S (bpv_result_bpvnedb_source_selected) = S ((S (e)) * ff_v_bpvnedb_source_selected_power_product)) /\ exists ff_q_bpvnedb_source_selected_power_product_terminal. ff_u_bpvnedb_source_selected_power_product = ff_q_bpvnedb_source_selected_power_product_terminal * S ((S (e)) * ff_v_bpvnedb_source_selected_power_product) + (bpv_result_bpvnedb_source_selected))) /\ forall ff_i_bpvnedb_source_selected_power_product. (exists ff_lt_bpvnedb_source_selected_power_product_bound. ff_lt_bpvnedb_source_selected_power_product_bound + S ff_i_bpvnedb_source_selected_power_product = e) -> exists ff_p_bpvnedb_source_selected_power_product ff_r_bpvnedb_source_selected_power_product ff_s_bpvnedb_source_selected_power_product. ((((exists ff_h_bpvnedb_source_selected_power_product_factor. ff_h_bpvnedb_source_selected_power_product_factor + S (ff_p_bpvnedb_source_selected_power_product) = S ((S (ff_i_bpvnedb_source_selected_power_product)) * ff_c_bpvnedb_source_selected_power)) /\ exists ff_q_bpvnedb_source_selected_power_product_factor. ff_b_bpvnedb_source_selected_power = ff_q_bpvnedb_source_selected_power_product_factor * S ((S (ff_i_bpvnedb_source_selected_power_product)) * ff_c_bpvnedb_source_selected_power) + (ff_p_bpvnedb_source_selected_power_product))) /\ ((((exists ff_h_bpvnedb_source_selected_power_product_partial. ff_h_bpvnedb_source_selected_power_product_partial + S (ff_r_bpvnedb_source_selected_power_product) = S ((S (ff_i_bpvnedb_source_selected_power_product)) * ff_v_bpvnedb_source_selected_power_product)) /\ exists ff_q_bpvnedb_source_selected_power_product_partial. ff_u_bpvnedb_source_selected_power_product = ff_q_bpvnedb_source_selected_power_product_partial * S ((S (ff_i_bpvnedb_source_selected_power_product)) * ff_v_bpvnedb_source_selected_power_product) + (ff_r_bpvnedb_source_selected_power_product))) /\ ((((exists ff_h_bpvnedb_source_selected_power_product_successor. ff_h_bpvnedb_source_selected_power_product_successor + S (ff_s_bpvnedb_source_selected_power_product) = S ((S (S ff_i_bpvnedb_source_selected_power_product)) * ff_v_bpvnedb_source_selected_power_product)) /\ exists ff_q_bpvnedb_source_selected_power_product_successor. ff_u_bpvnedb_source_selected_power_product = ff_q_bpvnedb_source_selected_power_product_successor * S ((S (S ff_i_bpvnedb_source_selected_power_product)) * ff_v_bpvnedb_source_selected_power_product) + (ff_s_bpvnedb_source_selected_power_product))) /\ ff_s_bpvnedb_source_selected_power_product = ff_r_bpvnedb_source_selected_power_product * ff_p_bpvnedb_source_selected_power_product)))))))) /\ (exists bpv_factor_bpvnedb_source_selected_divides. c = bpv_result_bpvnedb_source_selected * bpv_factor_bpvnedb_source_selected_divides)))) /\ forall bpv_candidate_bpvnedb_source. (exists bpv_gap_bpvnedb_source_candidate_bound. bpv_gap_bpvnedb_source_candidate_bound + bpv_candidate_bpvnedb_source = c) -> (exists bpv_result_bpvnedb_source_candidate. ((exists ff_b_bpvnedb_source_candidate_power ff_c_bpvnedb_source_candidate_power. ((forall ff_i_bpvnedb_source_candidate_power_repeat. (exists ff_lt_bpvnedb_source_candidate_power_repeat_bound. ff_lt_bpvnedb_source_candidate_power_repeat_bound + S ff_i_bpvnedb_source_candidate_power_repeat = bpv_candidate_bpvnedb_source) -> (((exists ff_h_bpvnedb_source_candidate_power_repeat_decoded. ff_h_bpvnedb_source_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bpvnedb_source_candidate_power_repeat)) * ff_c_bpvnedb_source_candidate_power)) /\ exists ff_q_bpvnedb_source_candidate_power_repeat_decoded. ff_b_bpvnedb_source_candidate_power = ff_q_bpvnedb_source_candidate_power_repeat_decoded * S ((S (ff_i_bpvnedb_source_candidate_power_repeat)) * ff_c_bpvnedb_source_candidate_power) + (p)))) /\ (exists ff_u_bpvnedb_source_candidate_power_product ff_v_bpvnedb_source_candidate_power_product. ((((exists ff_h_bpvnedb_source_candidate_power_product_start. ff_h_bpvnedb_source_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpvnedb_source_candidate_power_product)) /\ exists ff_q_bpvnedb_source_candidate_power_product_start. ff_u_bpvnedb_source_candidate_power_product = ff_q_bpvnedb_source_candidate_power_product_start * S ((S (0)) * ff_v_bpvnedb_source_candidate_power_product) + (1))) /\ ((((exists ff_h_bpvnedb_source_candidate_power_product_terminal. ff_h_bpvnedb_source_candidate_power_product_terminal + S (bpv_result_bpvnedb_source_candidate) = S ((S (bpv_candidate_bpvnedb_source)) * ff_v_bpvnedb_source_candidate_power_product)) /\ exists ff_q_bpvnedb_source_candidate_power_product_terminal. ff_u_bpvnedb_source_candidate_power_product = ff_q_bpvnedb_source_candidate_power_product_terminal * S ((S (bpv_candidate_bpvnedb_source)) * ff_v_bpvnedb_source_candidate_power_product) + (bpv_result_bpvnedb_source_candidate))) /\ forall ff_i_bpvnedb_source_candidate_power_product. (exists ff_lt_bpvnedb_source_candidate_power_product_bound. ff_lt_bpvnedb_source_candidate_power_product_bound + S ff_i_bpvnedb_source_candidate_power_product = bpv_candidate_bpvnedb_source) -> exists ff_p_bpvnedb_source_candidate_power_product ff_r_bpvnedb_source_candidate_power_product ff_s_bpvnedb_source_candidate_power_product. ((((exists ff_h_bpvnedb_source_candidate_power_product_factor. ff_h_bpvnedb_source_candidate_power_product_factor + S (ff_p_bpvnedb_source_candidate_power_product) = S ((S (ff_i_bpvnedb_source_candidate_power_product)) * ff_c_bpvnedb_source_candidate_power)) /\ exists ff_q_bpvnedb_source_candidate_power_product_factor. ff_b_bpvnedb_source_candidate_power = ff_q_bpvnedb_source_candidate_power_product_factor * S ((S (ff_i_bpvnedb_source_candidate_power_product)) * ff_c_bpvnedb_source_candidate_power) + (ff_p_bpvnedb_source_candidate_power_product))) /\ ((((exists ff_h_bpvnedb_source_candidate_power_product_partial. ff_h_bpvnedb_source_candidate_power_product_partial + S (ff_r_bpvnedb_source_candidate_power_product) = S ((S (ff_i_bpvnedb_source_candidate_power_product)) * ff_v_bpvnedb_source_candidate_power_product)) /\ exists ff_q_bpvnedb_source_candidate_power_product_partial. ff_u_bpvnedb_source_candidate_power_product = ff_q_bpvnedb_source_candidate_power_product_partial * S ((S (ff_i_bpvnedb_source_candidate_power_product)) * ff_v_bpvnedb_source_candidate_power_product) + (ff_r_bpvnedb_source_candidate_power_product))) /\ ((((exists ff_h_bpvnedb_source_candidate_power_product_successor. ff_h_bpvnedb_source_candidate_power_product_successor + S (ff_s_bpvnedb_source_candidate_power_product) = S ((S (S ff_i_bpvnedb_source_candidate_power_product)) * ff_v_bpvnedb_source_candidate_power_product)) /\ exists ff_q_bpvnedb_source_candidate_power_product_successor. ff_u_bpvnedb_source_candidate_power_product = ff_q_bpvnedb_source_candidate_power_product_successor * S ((S (S ff_i_bpvnedb_source_candidate_power_product)) * ff_v_bpvnedb_source_candidate_power_product) + (ff_s_bpvnedb_source_candidate_power_product))) /\ ff_s_bpvnedb_source_candidate_power_product = ff_r_bpvnedb_source_candidate_power_product * ff_p_bpvnedb_source_candidate_power_product)))))))) /\ (exists bpv_factor_bpvnedb_source_candidate_divides. c = bpv_result_bpvnedb_source_candidate * bpv_factor_bpvnedb_source_candidate_divides))) -> (exists bpv_gap_bpvnedb_source_maximal. bpv_gap_bpvnedb_source_maximal + bpv_candidate_bpvnedb_source = e)) -> ~(e = 0) -> (exists bpr_quotient_bpvnedb_result. c = (p) * bpr_quotient_bpvnedb_result)

Structural proof guide

A nonzero valuation exponent exposes the base as a divisor.

Direct prerequisites: one_le_of_ne_zero, power_valuation_power_divides, power_divides_exponent_antitone, pow_one. The authored body proceeds by case analysis (2), intermediate claims (4), equality transport (1).

Proof neighborhood

Direct dependencies

BT0010 one_le_of_ne_zero BT00Q9 power_valuation_power_divides BT00QK power_divides_exponent_antitone BT0094 pow_one

Direct dependents

BT00YJ no_bertrand_central_nonzero_valuation_live_ranges

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

34 script commands · 6 reading checkpoints · 4 local claims

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 (4)
one le of ne zeropower valuation power dividespower divides exponent antitonepow one

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro c
  3. L3
    intro e
  4. L4
    intro hvaluation
  5. L5
    intro hexponent
02Establish honeL6–9

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L6
    have hone : exists bpr_le_gap_bpvnedb_one_bound. bpr_le_gap_bpvnedb_one_bound + (1) = (e)
  2. L7
    specialize one_le_of_ne_zero e
  3. L8
    apply one_le_of_ne_zero
  4. L9
    exact hexponent
03Establish hselectedL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power valuation power divides.

  1. L10
    have hselected : PowerDivides(p,e,c)Definitions: PowerDivides
  2. L11
    specialize power_valuation_power_divides p
  3. L12
    specialize power_valuation_power_divides c
  4. L13
    specialize power_valuation_power_divides e
  5. L14
    apply power_valuation_power_divides
  6. L15
    exact hvaluation
04Establish hunitL16–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power divides exponent antitone.

  1. L16
    have hunit : PowerDivides(p,1,c)Definitions: PowerDivides
  2. L17
    specialize power_divides_exponent_antitone p
  3. L18
    specialize power_divides_exponent_antitone 1
  4. L19
    specialize power_divides_exponent_antitone e
  5. L20
    specialize power_divides_exponent_antitone c
  6. L21
    apply power_divides_exponent_antitone
  7. L22
    exact hone
  8. L23
    exact hselected
05Separate the logical casesL24–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L24
    cases hunit
  2. L25
    cases hunit_witness
06Establish hvalueL26–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow one.

  1. L26
    have hvalue : x = p
  2. L27
    specialize pow_one p
  3. L28
    specialize pow_one 1
  4. L29
    specialize pow_one x
  5. L30
    apply pow_one
  6. L31
    refl
  7. L32
    exact hunit_witness_left
  8. L33
    rewrite hvalue at hunit_witness_right
  9. L34
    exact hunit_witness_right

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro p
  2. 0002intro c
  3. 0003intro e
  4. 0004intro hvaluation
  5. 0005intro hexponent
  6. 0006have hone : exists bpr_le_gap_bpvnedb_one_bound. bpr_le_gap_bpvnedb_one_bound + (1) = (e)
  7. 0007specialize one_le_of_ne_zero e
  8. 0008apply one_le_of_ne_zero
  9. 0009exact hexponent
  10. 0010have hselected : exists bpvi_result_bpvnedb_selected. ((exists bpvi_b_bpvnedb_selected_power bpvi_c_bpvnedb_selected_power. ((forall bpvi_i_bpvnedb_selected_power. (exists bpvi_repeat_gap_bpvnedb_selected_power. bpvi_repeat_gap_bpvnedb_selected_power + S bpvi_i_bpvnedb_selected_power = e) -> (((exists bpvi_h_bpvnedb_selected_power_repeat. bpvi_h_bpvnedb_selected_power_repeat + S (p) = S ((S (bpvi_i_bpvnedb_selected_power)) * bpvi_c_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_repeat. bpvi_b_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_repeat * S ((S (bpvi_i_bpvnedb_selected_power)) * bpvi_c_bpvnedb_selected_power) + (p)))) /\ (exists bpvi_u_bpvnedb_selected_power bpvi_v_bpvnedb_selected_power. ((((exists bpvi_h_bpvnedb_selected_power_start. bpvi_h_bpvnedb_selected_power_start + S (1) = S ((S (0)) * bpvi_v_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_start. bpvi_u_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_start * S ((S (0)) * bpvi_v_bpvnedb_selected_power) + (1))) /\ ((((exists bpvi_h_bpvnedb_selected_power_terminal. bpvi_h_bpvnedb_selected_power_terminal + S (bpvi_result_bpvnedb_selected) = S ((S (e)) * bpvi_v_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_terminal. bpvi_u_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_terminal * S ((S (e)) * bpvi_v_bpvnedb_selected_power) + (bpvi_result_bpvnedb_selected))) /\ forall bpvi_j_bpvnedb_selected_power. (exists bpvi_product_gap_bpvnedb_selected_power. bpvi_product_gap_bpvnedb_selected_power + S bpvi_j_bpvnedb_selected_power = e) -> exists bpvi_factor_bpvnedb_selected_power bpvi_partial_bpvnedb_selected_power bpvi_successor_bpvnedb_selected_power. ((((exists bpvi_h_bpvnedb_selected_power_factor. bpvi_h_bpvnedb_selected_power_factor + S (bpvi_factor_bpvnedb_selected_power) = S ((S (bpvi_j_bpvnedb_selected_power)) * bpvi_c_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_factor. bpvi_b_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_factor * S ((S (bpvi_j_bpvnedb_selected_power)) * bpvi_c_bpvnedb_selected_power) + (bpvi_factor_bpvnedb_selected_power))) /\ ((((exists bpvi_h_bpvnedb_selected_power_partial. bpvi_h_bpvnedb_selected_power_partial + S (bpvi_partial_bpvnedb_selected_power) = S ((S (bpvi_j_bpvnedb_selected_power)) * bpvi_v_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_partial. bpvi_u_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_partial * S ((S (bpvi_j_bpvnedb_selected_power)) * bpvi_v_bpvnedb_selected_power) + (bpvi_partial_bpvnedb_selected_power))) /\ ((((exists bpvi_h_bpvnedb_selected_power_successor. bpvi_h_bpvnedb_selected_power_successor + S (bpvi_successor_bpvnedb_selected_power) = S ((S (S bpvi_j_bpvnedb_selected_power)) * bpvi_v_bpvnedb_selected_power)) /\ exists bpvi_q_bpvnedb_selected_power_successor. bpvi_u_bpvnedb_selected_power = bpvi_q_bpvnedb_selected_power_successor * S ((S (S bpvi_j_bpvnedb_selected_power)) * bpvi_v_bpvnedb_selected_power) + (bpvi_successor_bpvnedb_selected_power))) /\ bpvi_successor_bpvnedb_selected_power = bpvi_partial_bpvnedb_selected_power * bpvi_factor_bpvnedb_selected_power)))))))) /\ exists bpvi_divisor_factor_bpvnedb_selected. c = bpvi_result_bpvnedb_selected * bpvi_divisor_factor_bpvnedb_selected)
  11. 0011specialize power_valuation_power_divides p
  12. 0012specialize power_valuation_power_divides c
  13. 0013specialize power_valuation_power_divides e
  14. 0014apply power_valuation_power_divides
  15. 0015exact hvaluation
  16. 0016have hunit : exists bpvi_result_bpvnedb_unit. ((exists bpvi_b_bpvnedb_unit_power bpvi_c_bpvnedb_unit_power. ((forall bpvi_i_bpvnedb_unit_power. (exists bpvi_repeat_gap_bpvnedb_unit_power. bpvi_repeat_gap_bpvnedb_unit_power + S bpvi_i_bpvnedb_unit_power = 1) -> (((exists bpvi_h_bpvnedb_unit_power_repeat. bpvi_h_bpvnedb_unit_power_repeat + S (p) = S ((S (bpvi_i_bpvnedb_unit_power)) * bpvi_c_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_repeat. bpvi_b_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_repeat * S ((S (bpvi_i_bpvnedb_unit_power)) * bpvi_c_bpvnedb_unit_power) + (p)))) /\ (exists bpvi_u_bpvnedb_unit_power bpvi_v_bpvnedb_unit_power. ((((exists bpvi_h_bpvnedb_unit_power_start. bpvi_h_bpvnedb_unit_power_start + S (1) = S ((S (0)) * bpvi_v_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_start. bpvi_u_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_start * S ((S (0)) * bpvi_v_bpvnedb_unit_power) + (1))) /\ ((((exists bpvi_h_bpvnedb_unit_power_terminal. bpvi_h_bpvnedb_unit_power_terminal + S (bpvi_result_bpvnedb_unit) = S ((S (1)) * bpvi_v_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_terminal. bpvi_u_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_terminal * S ((S (1)) * bpvi_v_bpvnedb_unit_power) + (bpvi_result_bpvnedb_unit))) /\ forall bpvi_j_bpvnedb_unit_power. (exists bpvi_product_gap_bpvnedb_unit_power. bpvi_product_gap_bpvnedb_unit_power + S bpvi_j_bpvnedb_unit_power = 1) -> exists bpvi_factor_bpvnedb_unit_power bpvi_partial_bpvnedb_unit_power bpvi_successor_bpvnedb_unit_power. ((((exists bpvi_h_bpvnedb_unit_power_factor. bpvi_h_bpvnedb_unit_power_factor + S (bpvi_factor_bpvnedb_unit_power) = S ((S (bpvi_j_bpvnedb_unit_power)) * bpvi_c_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_factor. bpvi_b_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_factor * S ((S (bpvi_j_bpvnedb_unit_power)) * bpvi_c_bpvnedb_unit_power) + (bpvi_factor_bpvnedb_unit_power))) /\ ((((exists bpvi_h_bpvnedb_unit_power_partial. bpvi_h_bpvnedb_unit_power_partial + S (bpvi_partial_bpvnedb_unit_power) = S ((S (bpvi_j_bpvnedb_unit_power)) * bpvi_v_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_partial. bpvi_u_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_partial * S ((S (bpvi_j_bpvnedb_unit_power)) * bpvi_v_bpvnedb_unit_power) + (bpvi_partial_bpvnedb_unit_power))) /\ ((((exists bpvi_h_bpvnedb_unit_power_successor. bpvi_h_bpvnedb_unit_power_successor + S (bpvi_successor_bpvnedb_unit_power) = S ((S (S bpvi_j_bpvnedb_unit_power)) * bpvi_v_bpvnedb_unit_power)) /\ exists bpvi_q_bpvnedb_unit_power_successor. bpvi_u_bpvnedb_unit_power = bpvi_q_bpvnedb_unit_power_successor * S ((S (S bpvi_j_bpvnedb_unit_power)) * bpvi_v_bpvnedb_unit_power) + (bpvi_successor_bpvnedb_unit_power))) /\ bpvi_successor_bpvnedb_unit_power = bpvi_partial_bpvnedb_unit_power * bpvi_factor_bpvnedb_unit_power)))))))) /\ exists bpvi_divisor_factor_bpvnedb_unit. c = bpvi_result_bpvnedb_unit * bpvi_divisor_factor_bpvnedb_unit)
  17. 0017specialize power_divides_exponent_antitone p
  18. 0018specialize power_divides_exponent_antitone 1
  19. 0019specialize power_divides_exponent_antitone e
  20. 0020specialize power_divides_exponent_antitone c
  21. 0021apply power_divides_exponent_antitone
  22. 0022exact hone
  23. 0023exact hselected
  24. 0024cases hunit
  25. 0025cases hunit_witness
  26. 0026have hvalue : x = p
  27. 0027specialize pow_one p
  28. 0028specialize pow_one 1
  29. 0029specialize pow_one x
  30. 0030apply pow_one
  31. 0031refl
  32. 0032exact hunit_witness_left
  33. 0033rewrite hvalue at hunit_witness_right
  34. 0034exact hunit_witness_right