EL000A

lte_power_difference_second_order_exists

Construct the real powers, difference quotient, first correction, and doubled triangular correction at every exponent at least two.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ d. ∀ k. a = b + d → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ i. ∃ j. PowerDifferenceSecondOrder(a,b,d,k,x,y,z,n,m,i,j)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H) · 2

Actual proof prerequisites

lte_power_zero_exactlte_power_one_exactlte_power_two_exactlte_natural_difference_squarelte_natural_difference_successorlte_first_correction_successorlte_twice_correction_successorpow_successor_pair_mul · checked external prerequisitepow_successor_compose · checked external prerequisitemul_comm · checked external prerequisitemul_one · checked external prerequisiteadd_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitemul_succ_left · checked external prerequisitemul_zero_left · checked external prerequisitezero_add · checked external prerequisiteone_mul · checked external prerequisite
Original expanded first-order statement 
forall a b d k. a = b + d -> exists A B R T Q C H. (((exists pa_b_olte_resultA pa_c_olte_resultA. ((forall pa_i_olte_resultA_repeat. (exists pa_lt_olte_resultA_repeat_bound. pa_lt_olte_resultA_repeat_bound + S pa_i_olte_resultA_repeat = S (S (k))) -> (((exists pa_h_olte_resultA_repeat_decoded. pa_h_olte_resultA_repeat_decoded + S (a) = S ((S (pa_i_olte_resultA_repeat)) * pa_c_olte_resultA)) /\ exists pa_q_olte_resultA_repeat_decoded. pa_b_olte_resultA = pa_q_olte_resultA_repeat_decoded * S ((S (pa_i_olte_resultA_repeat)) * pa_c_olte_resultA) + (a)))) /\ (exists pa_u_olte_resultA_product pa_v_olte_resultA_product. ((((exists pa_h_olte_resultA_product_start. pa_h_olte_resultA_product_start + S (1) = S ((S (0)) * pa_v_olte_resultA_product)) /\ exists pa_q_olte_resultA_product_start. pa_u_olte_resultA_product = pa_q_olte_resultA_product_start * S ((S (0)) * pa_v_olte_resultA_product) + (1))) /\ ((((exists pa_h_olte_resultA_product_terminal. pa_h_olte_resultA_product_terminal + S (A) = S ((S (S (S (k)))) * pa_v_olte_resultA_product)) /\ exists pa_q_olte_resultA_product_terminal. pa_u_olte_resultA_product = pa_q_olte_resultA_product_terminal * S ((S (S (S (k)))) * pa_v_olte_resultA_product) + (A))) /\ forall pa_i_olte_resultA_product. (exists pa_lt_olte_resultA_product_bound. pa_lt_olte_resultA_product_bound + S pa_i_olte_resultA_product = S (S (k))) -> exists pa_p_olte_resultA_product pa_r_olte_resultA_product pa_s_olte_resultA_product. ((((exists pa_h_olte_resultA_product_factor. pa_h_olte_resultA_product_factor + S (pa_p_olte_resultA_product) = S ((S (pa_i_olte_resultA_product)) * pa_c_olte_resultA)) /\ exists pa_q_olte_resultA_product_factor. pa_b_olte_resultA = pa_q_olte_resultA_product_factor * S ((S (pa_i_olte_resultA_product)) * pa_c_olte_resultA) + (pa_p_olte_resultA_product))) /\ ((((exists pa_h_olte_resultA_product_partial. pa_h_olte_resultA_product_partial + S (pa_r_olte_resultA_product) = S ((S (pa_i_olte_resultA_product)) * pa_v_olte_resultA_product)) /\ exists pa_q_olte_resultA_product_partial. pa_u_olte_resultA_product = pa_q_olte_resultA_product_partial * S ((S (pa_i_olte_resultA_product)) * pa_v_olte_resultA_product) + (pa_r_olte_resultA_product))) /\ ((((exists pa_h_olte_resultA_product_successor. pa_h_olte_resultA_product_successor + S (pa_s_olte_resultA_product) = S ((S (S pa_i_olte_resultA_product)) * pa_v_olte_resultA_product)) /\ exists pa_q_olte_resultA_product_successor. pa_u_olte_resultA_product = pa_q_olte_resultA_product_successor * S ((S (S pa_i_olte_resultA_product)) * pa_v_olte_resultA_product) + (pa_s_olte_resultA_product))) /\ pa_s_olte_resultA_product = pa_r_olte_resultA_product * pa_p_olte_resultA_product)))))))) /\ (((exists pa_b_olte_resultB pa_c_olte_resultB. ((forall pa_i_olte_resultB_repeat. (exists pa_lt_olte_resultB_repeat_bound. pa_lt_olte_resultB_repeat_bound + S pa_i_olte_resultB_repeat = S (S (k))) -> (((exists pa_h_olte_resultB_repeat_decoded. pa_h_olte_resultB_repeat_decoded + S (b) = S ((S (pa_i_olte_resultB_repeat)) * pa_c_olte_resultB)) /\ exists pa_q_olte_resultB_repeat_decoded. pa_b_olte_resultB = pa_q_olte_resultB_repeat_decoded * S ((S (pa_i_olte_resultB_repeat)) * pa_c_olte_resultB) + (b)))) /\ (exists pa_u_olte_resultB_product pa_v_olte_resultB_product. ((((exists pa_h_olte_resultB_product_start. pa_h_olte_resultB_product_start + S (1) = S ((S (0)) * pa_v_olte_resultB_product)) /\ exists pa_q_olte_resultB_product_start. pa_u_olte_resultB_product = pa_q_olte_resultB_product_start * S ((S (0)) * pa_v_olte_resultB_product) + (1))) /\ ((((exists pa_h_olte_resultB_product_terminal. pa_h_olte_resultB_product_terminal + S (B) = S ((S (S (S (k)))) * pa_v_olte_resultB_product)) /\ exists pa_q_olte_resultB_product_terminal. pa_u_olte_resultB_product = pa_q_olte_resultB_product_terminal * S ((S (S (S (k)))) * pa_v_olte_resultB_product) + (B))) /\ forall pa_i_olte_resultB_product. (exists pa_lt_olte_resultB_product_bound. pa_lt_olte_resultB_product_bound + S pa_i_olte_resultB_product = S (S (k))) -> exists pa_p_olte_resultB_product pa_r_olte_resultB_product pa_s_olte_resultB_product. ((((exists pa_h_olte_resultB_product_factor. pa_h_olte_resultB_product_factor + S (pa_p_olte_resultB_product) = S ((S (pa_i_olte_resultB_product)) * pa_c_olte_resultB)) /\ exists pa_q_olte_resultB_product_factor. pa_b_olte_resultB = pa_q_olte_resultB_product_factor * S ((S (pa_i_olte_resultB_product)) * pa_c_olte_resultB) + (pa_p_olte_resultB_product))) /\ ((((exists pa_h_olte_resultB_product_partial. pa_h_olte_resultB_product_partial + S (pa_r_olte_resultB_product) = S ((S (pa_i_olte_resultB_product)) * pa_v_olte_resultB_product)) /\ exists pa_q_olte_resultB_product_partial. pa_u_olte_resultB_product = pa_q_olte_resultB_product_partial * S ((S (pa_i_olte_resultB_product)) * pa_v_olte_resultB_product) + (pa_r_olte_resultB_product))) /\ ((((exists pa_h_olte_resultB_product_successor. pa_h_olte_resultB_product_successor + S (pa_s_olte_resultB_product) = S ((S (S pa_i_olte_resultB_product)) * pa_v_olte_resultB_product)) /\ exists pa_q_olte_resultB_product_successor. pa_u_olte_resultB_product = pa_q_olte_resultB_product_successor * S ((S (S pa_i_olte_resultB_product)) * pa_v_olte_resultB_product) + (pa_s_olte_resultB_product))) /\ pa_s_olte_resultB_product = pa_r_olte_resultB_product * pa_p_olte_resultB_product)))))))) /\ (((exists pa_b_olte_resultR pa_c_olte_resultR. ((forall pa_i_olte_resultR_repeat. (exists pa_lt_olte_resultR_repeat_bound. pa_lt_olte_resultR_repeat_bound + S pa_i_olte_resultR_repeat = S (k)) -> (((exists pa_h_olte_resultR_repeat_decoded. pa_h_olte_resultR_repeat_decoded + S (b) = S ((S (pa_i_olte_resultR_repeat)) * pa_c_olte_resultR)) /\ exists pa_q_olte_resultR_repeat_decoded. pa_b_olte_resultR = pa_q_olte_resultR_repeat_decoded * S ((S (pa_i_olte_resultR_repeat)) * pa_c_olte_resultR) + (b)))) /\ (exists pa_u_olte_resultR_product pa_v_olte_resultR_product. ((((exists pa_h_olte_resultR_product_start. pa_h_olte_resultR_product_start + S (1) = S ((S (0)) * pa_v_olte_resultR_product)) /\ exists pa_q_olte_resultR_product_start. pa_u_olte_resultR_product = pa_q_olte_resultR_product_start * S ((S (0)) * pa_v_olte_resultR_product) + (1))) /\ ((((exists pa_h_olte_resultR_product_terminal. pa_h_olte_resultR_product_terminal + S (R) = S ((S (S (k))) * pa_v_olte_resultR_product)) /\ exists pa_q_olte_resultR_product_terminal. pa_u_olte_resultR_product = pa_q_olte_resultR_product_terminal * S ((S (S (k))) * pa_v_olte_resultR_product) + (R))) /\ forall pa_i_olte_resultR_product. (exists pa_lt_olte_resultR_product_bound. pa_lt_olte_resultR_product_bound + S pa_i_olte_resultR_product = S (k)) -> exists pa_p_olte_resultR_product pa_r_olte_resultR_product pa_s_olte_resultR_product. ((((exists pa_h_olte_resultR_product_factor. pa_h_olte_resultR_product_factor + S (pa_p_olte_resultR_product) = S ((S (pa_i_olte_resultR_product)) * pa_c_olte_resultR)) /\ exists pa_q_olte_resultR_product_factor. pa_b_olte_resultR = pa_q_olte_resultR_product_factor * S ((S (pa_i_olte_resultR_product)) * pa_c_olte_resultR) + (pa_p_olte_resultR_product))) /\ ((((exists pa_h_olte_resultR_product_partial. pa_h_olte_resultR_product_partial + S (pa_r_olte_resultR_product) = S ((S (pa_i_olte_resultR_product)) * pa_v_olte_resultR_product)) /\ exists pa_q_olte_resultR_product_partial. pa_u_olte_resultR_product = pa_q_olte_resultR_product_partial * S ((S (pa_i_olte_resultR_product)) * pa_v_olte_resultR_product) + (pa_r_olte_resultR_product))) /\ ((((exists pa_h_olte_resultR_product_successor. pa_h_olte_resultR_product_successor + S (pa_s_olte_resultR_product) = S ((S (S pa_i_olte_resultR_product)) * pa_v_olte_resultR_product)) /\ exists pa_q_olte_resultR_product_successor. pa_u_olte_resultR_product = pa_q_olte_resultR_product_successor * S ((S (S pa_i_olte_resultR_product)) * pa_v_olte_resultR_product) + (pa_s_olte_resultR_product))) /\ pa_s_olte_resultR_product = pa_r_olte_resultR_product * pa_p_olte_resultR_product)))))))) /\ (((exists pa_b_olte_resultT pa_c_olte_resultT. ((forall pa_i_olte_resultT_repeat. (exists pa_lt_olte_resultT_repeat_bound. pa_lt_olte_resultT_repeat_bound + S pa_i_olte_resultT_repeat = k) -> (((exists pa_h_olte_resultT_repeat_decoded. pa_h_olte_resultT_repeat_decoded + S (b) = S ((S (pa_i_olte_resultT_repeat)) * pa_c_olte_resultT)) /\ exists pa_q_olte_resultT_repeat_decoded. pa_b_olte_resultT = pa_q_olte_resultT_repeat_decoded * S ((S (pa_i_olte_resultT_repeat)) * pa_c_olte_resultT) + (b)))) /\ (exists pa_u_olte_resultT_product pa_v_olte_resultT_product. ((((exists pa_h_olte_resultT_product_start. pa_h_olte_resultT_product_start + S (1) = S ((S (0)) * pa_v_olte_resultT_product)) /\ exists pa_q_olte_resultT_product_start. pa_u_olte_resultT_product = pa_q_olte_resultT_product_start * S ((S (0)) * pa_v_olte_resultT_product) + (1))) /\ ((((exists pa_h_olte_resultT_product_terminal. pa_h_olte_resultT_product_terminal + S (T) = S ((S (k)) * pa_v_olte_resultT_product)) /\ exists pa_q_olte_resultT_product_terminal. pa_u_olte_resultT_product = pa_q_olte_resultT_product_terminal * S ((S (k)) * pa_v_olte_resultT_product) + (T))) /\ forall pa_i_olte_resultT_product. (exists pa_lt_olte_resultT_product_bound. pa_lt_olte_resultT_product_bound + S pa_i_olte_resultT_product = k) -> exists pa_p_olte_resultT_product pa_r_olte_resultT_product pa_s_olte_resultT_product. ((((exists pa_h_olte_resultT_product_factor. pa_h_olte_resultT_product_factor + S (pa_p_olte_resultT_product) = S ((S (pa_i_olte_resultT_product)) * pa_c_olte_resultT)) /\ exists pa_q_olte_resultT_product_factor. pa_b_olte_resultT = pa_q_olte_resultT_product_factor * S ((S (pa_i_olte_resultT_product)) * pa_c_olte_resultT) + (pa_p_olte_resultT_product))) /\ ((((exists pa_h_olte_resultT_product_partial. pa_h_olte_resultT_product_partial + S (pa_r_olte_resultT_product) = S ((S (pa_i_olte_resultT_product)) * pa_v_olte_resultT_product)) /\ exists pa_q_olte_resultT_product_partial. pa_u_olte_resultT_product = pa_q_olte_resultT_product_partial * S ((S (pa_i_olte_resultT_product)) * pa_v_olte_resultT_product) + (pa_r_olte_resultT_product))) /\ ((((exists pa_h_olte_resultT_product_successor. pa_h_olte_resultT_product_successor + S (pa_s_olte_resultT_product) = S ((S (S pa_i_olte_resultT_product)) * pa_v_olte_resultT_product)) /\ exists pa_q_olte_resultT_product_successor. pa_u_olte_resultT_product = pa_q_olte_resultT_product_successor * S ((S (S pa_i_olte_resultT_product)) * pa_v_olte_resultT_product) + (pa_s_olte_resultT_product))) /\ pa_s_olte_resultT_product = pa_r_olte_resultT_product * pa_p_olte_resultT_product)))))))) /\ ((((A) = (B) + (d) * (Q)) /\ ((((Q) = S (S (k)) * (R) + (d) * (C)) /\ (2 * (C) = (S (S (k)) * S (k)) * (T) + (d) * (H))))))))))))))

Complete tactic proof in conservative notation

All 164 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

164 script commands · 45 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (7)
lte power two exactlte power one exactlte power zero exactlte natural difference squarelte natural difference successorlte first correction successorlte twice correction successor
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro d
02Induction on kL4–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction k
  2. L5
    intro ha
03Construct an explicit witnessL6–12

Supply the displayed value, then prove that it has the required property.

  1. L6
    exists a * a
  2. L7
    exists b * b
  3. L8
    exists b
  4. L9
    exists 1
  5. L10
    exists a + b
  6. L11
    exists 1
  7. L12
    exists 0
04Separate the logical casesL13–13

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

  1. L13
    split
05Use earlier factsL14–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L14
    specialize lte_power_two_exact (a)
  2. L15
    apply lte_power_two_exact
06Separate the logical casesL16–16

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

  1. L16
    split
07Use earlier factsL17–18

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    specialize lte_power_two_exact (b)
  2. L18
    apply lte_power_two_exact
08Separate the logical casesL19–19

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

  1. L19
    split
09Use earlier factsL20–21

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L20
    specialize lte_power_one_exact (b)
  2. L21
    apply lte_power_one_exact
10Separate the logical casesL22–22

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

  1. L22
    split
11Use earlier factsL23–24

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize lte_power_zero_exact (b)
  2. L24
    apply lte_power_zero_exact
12Separate the logical casesL25–25

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

  1. L25
    split
13Use earlier factsL26–30

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    specialize lte_natural_difference_square (a)
  2. L27
    specialize lte_natural_difference_square (b)
  3. L28
    specialize lte_natural_difference_square (d)
  4. L29
    apply lte_natural_difference_square
  5. L30
    exact ha
14Separate the logical casesL31–31

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

  1. L31
    split
15Calculate and transport equalitiesL32–41

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L32
    rewrite ha
  2. L33
    trans ((b) + ((d) + (b)))
  3. L34
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  4. L35
    trans ((b) + ((d) + (b)))
  5. L36
    congr
  6. L37
    refl
  7. L38
    congr
  8. L39
    refl
  9. L40
    refl
  10. L41
    trans ((b) + ((b) + (d)))
16Calculate and transport equalitiesL42–44

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    congr
  2. L43
    refl
  3. L44
    trans ((b) + (d))
17Use earlier factsL45–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    apply add_comm
18Calculate and transport equalitiesL46–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L46
    congr
  2. L47
    refl
  3. L48
    refl
  4. L49
    trans ((b) + ((b) + (d)))
  5. L50
    symm
  6. L51
    congr
  7. L52
    refl
  8. L53
    congr
  9. L54
    refl
  10. L55
    refl
19Calculate and transport equalitiesL56–58

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L56
    symm
  2. L57
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  3. L58
    simp [mul_one]
20Fix variables and assumptionsL59–59

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

  1. L59
    intro ha
21Establish hprefixL60–62

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

  1. L60
    have hprefix : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H)Definitions: PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H)Original native command in the exact edition
  2. L61
    apply IH
  3. L62
    exact ha
22Separate the logical casesL63–72

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

  1. L63
    cases hprefix
  2. L64
    cases hprefix_witness
  3. L65
    cases hprefix_witness_witness
  4. L66
    cases hprefix_witness_witness_witness
  5. L67
    cases hprefix_witness_witness_witness_witness
  6. L68
    cases hprefix_witness_witness_witness_witness_witness
  7. L69
    cases hprefix_witness_witness_witness_witness_witness_witness
  8. L70
    cases hprefix_witness_witness_witness_witness_witness_witness_witness
  9. L71
    cases hprefix_witness_witness_witness_witness_witness_witness_witness_right
  10. L72
    cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right
23Separate the logical casesL73–75

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

  1. L73
    cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right
  2. L74
    cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  3. L75
    cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
24Establish hBL76–85

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

  1. L76
    have hB : x1 = b * x2
  2. L77
    trans x2 * b
  3. L78
    specialize pow_successor_pair_mul (b)
  4. L79
    specialize pow_successor_pair_mul (S k)
  5. L80
    specialize pow_successor_pair_mul (S (S k))
  6. L81
    specialize pow_successor_pair_mul (x2)
  7. L82
    specialize pow_successor_pair_mul (x1)
  8. L83
    apply pow_successor_pair_mul
  9. L84
    refl
  10. L85
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
25Use earlier factsL86–87

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L86
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L87
    apply mul_comm
26Establish hRL88–97

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

  1. L88
    have hR : x2 = b * x3
  2. L89
    trans x3 * b
  3. L90
    specialize pow_successor_pair_mul (b)
  4. L91
    specialize pow_successor_pair_mul (k)
  5. L92
    specialize pow_successor_pair_mul (S k)
  6. L93
    specialize pow_successor_pair_mul (x3)
  7. L94
    specialize pow_successor_pair_mul (x2)
  8. L95
    apply pow_successor_pair_mul
  9. L96
    refl
  10. L97
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
27Use earlier factsL98–99

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L98
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
  2. L99
    apply mul_comm
28Construct an explicit witnessL100–106

Supply the displayed value, then prove that it has the required property.

  1. L100
    exists a * x
  2. L101
    exists b * x1
  3. L102
    exists x1
  4. L103
    exists x2
  5. L104
    exists a * x4 + x1
  6. L105
    exists b * x5 + x4
  7. L106
    exists b * x6 + 2 * x5
29Separate the logical casesL107–107

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

  1. L107
    split
30Use earlier factsL108–114

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L108
    specialize pow_successor_compose (a)
  2. L109
    specialize pow_successor_compose (S (S k))
  3. L110
    specialize pow_successor_compose (x)
  4. L111
    specialize pow_successor_compose (a * x)
  5. L112
    apply pow_successor_compose
  6. L113
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_left
  7. L114
    apply mul_comm
31Separate the logical casesL115–115

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

  1. L115
    split
32Use earlier factsL116–122

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L116
    specialize pow_successor_compose (b)
  2. L117
    specialize pow_successor_compose (S (S k))
  3. L118
    specialize pow_successor_compose (x1)
  4. L119
    specialize pow_successor_compose (b * x1)
  5. L120
    apply pow_successor_compose
  6. L121
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
  7. L122
    apply mul_comm
33Separate the logical casesL123–123

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

  1. L123
    split
34Use earlier factsL124–124

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L124
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
35Separate the logical casesL125–125

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

  1. L125
    split
36Use earlier factsL126–126

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L126
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
37Separate the logical casesL127–127

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

  1. L127
    split
38Calculate and transport equalitiesL128–128

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L128
    rewrite hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
39Use earlier factsL129–135

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L129
    specialize lte_natural_difference_successor (a)
  2. L130
    specialize lte_natural_difference_successor (b)
  3. L131
    specialize lte_natural_difference_successor (d)
  4. L132
    specialize lte_natural_difference_successor (x1)
  5. L133
    specialize lte_natural_difference_successor (x4)
  6. L134
    apply lte_natural_difference_successor
  7. L135
    exact ha
40Separate the logical casesL136–136

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

  1. L136
    split
41Calculate and transport equalitiesL137–138

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L137
    rewrite hB
  2. L138
    rewrite hB
42Use earlier factsL139–148

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L139
    specialize lte_first_correction_successor (a)
  2. L140
    specialize lte_first_correction_successor (b)
  3. L141
    specialize lte_first_correction_successor (d)
  4. L142
    specialize lte_first_correction_successor (S (S k))
  5. L143
    specialize lte_first_correction_successor (x2)
  6. L144
    specialize lte_first_correction_successor (x4)
  7. L145
    specialize lte_first_correction_successor (x5)
  8. L146
    apply lte_first_correction_successor
  9. L147
    exact ha
  10. L148
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
43Calculate and transport equalitiesL149–149

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L149
    rewrite hR
44Establish hfirstL150–159

Establish this local claim before using it. It is not an additional assumption.

  1. L150
    have hfirst : x4 = S (S k) * (b * x3) + d * x5
  2. L151
    trans S (S k) * x2 + d * x5
  3. L152
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  4. L153
    rewrite hR
  5. L154
    refl
  6. L155
    specialize lte_twice_correction_successor (b)
  7. L156
    specialize lte_twice_correction_successor (d)
  8. L157
    specialize lte_twice_correction_successor (S k)
  9. L158
    specialize lte_twice_correction_successor (x3)
  10. L159
    specialize lte_twice_correction_successor (x5)
45Use earlier factsL160–164

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L160
    specialize lte_twice_correction_successor (x4)
  2. L161
    specialize lte_twice_correction_successor (x6)
  3. L162
    apply lte_twice_correction_successor
  4. L163
    exact hfirst
  5. L164
    exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 164 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro d
  4. 0004induction k
  5. 0005intro ha
  6. 0006exists a * a
  7. 0007exists b * b
  8. 0008exists b
  9. 0009exists 1
  10. 0010exists a + b
  11. 0011exists 1
  12. 0012exists 0
  13. 0013split
  14. 0014specialize lte_power_two_exact (a)
  15. 0015apply lte_power_two_exact
  16. 0016split
  17. 0017specialize lte_power_two_exact (b)
  18. 0018apply lte_power_two_exact
  19. 0019split
  20. 0020specialize lte_power_one_exact (b)
  21. 0021apply lte_power_one_exact
  22. 0022split
  23. 0023specialize lte_power_zero_exact (b)
  24. 0024apply lte_power_zero_exact
  25. 0025split
  26. 0026specialize lte_natural_difference_square (a)
  27. 0027specialize lte_natural_difference_square (b)
  28. 0028specialize lte_natural_difference_square (d)
  29. 0029apply lte_natural_difference_square
  30. 0030exact ha
  31. 0031split
  32. 0032rewrite ha
  33. 0033trans ((b) + ((d) + (b)))
  34. 0034simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  35. 0035trans ((b) + ((d) + (b)))
  36. 0036congr
  37. 0037refl
  38. 0038congr
  39. 0039refl
  40. 0040refl
  41. 0041trans ((b) + ((b) + (d)))
  42. 0042congr
  43. 0043refl
  44. 0044trans ((b) + (d))
  45. 0045apply add_comm
  46. 0046congr
  47. 0047refl
  48. 0048refl
  49. 0049trans ((b) + ((b) + (d)))
  50. 0050symm
  51. 0051congr
  52. 0052refl
  53. 0053congr
  54. 0054refl
  55. 0055refl
  56. 0056symm
  57. 0057simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  58. 0058simp [mul_one]
  59. 0059intro ha
  60. 0060have hprefix : ∃ A. ∃ B. ∃ R. ∃ T. ∃ Q. ∃ C. ∃ H. PowerDifferenceSecondOrder(a,b,d,k,A,B,R,T,Q,C,H)
  61. 0061apply IH
  62. 0062exact ha
  63. 0063cases hprefix
  64. 0064cases hprefix_witness
  65. 0065cases hprefix_witness_witness
  66. 0066cases hprefix_witness_witness_witness
  67. 0067cases hprefix_witness_witness_witness_witness
  68. 0068cases hprefix_witness_witness_witness_witness_witness
  69. 0069cases hprefix_witness_witness_witness_witness_witness_witness
  70. 0070cases hprefix_witness_witness_witness_witness_witness_witness_witness
  71. 0071cases hprefix_witness_witness_witness_witness_witness_witness_witness_right
  72. 0072cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right
  73. 0073cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right
  74. 0074cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right
  75. 0075cases hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right
  76. 0076have hB : x1 = b * x2
  77. 0077trans x2 * b
  78. 0078specialize pow_successor_pair_mul (b)
  79. 0079specialize pow_successor_pair_mul (S k)
  80. 0080specialize pow_successor_pair_mul (S (S k))
  81. 0081specialize pow_successor_pair_mul (x2)
  82. 0082specialize pow_successor_pair_mul (x1)
  83. 0083apply pow_successor_pair_mul
  84. 0084refl
  85. 0085exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
  86. 0086exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
  87. 0087apply mul_comm
  88. 0088have hR : x2 = b * x3
  89. 0089trans x3 * b
  90. 0090specialize pow_successor_pair_mul (b)
  91. 0091specialize pow_successor_pair_mul (k)
  92. 0092specialize pow_successor_pair_mul (S k)
  93. 0093specialize pow_successor_pair_mul (x3)
  94. 0094specialize pow_successor_pair_mul (x2)
  95. 0095apply pow_successor_pair_mul
  96. 0096refl
  97. 0097exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_left
  98. 0098exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
  99. 0099apply mul_comm
  100. 0100exists a * x
  101. 0101exists b * x1
  102. 0102exists x1
  103. 0103exists x2
  104. 0104exists a * x4 + x1
  105. 0105exists b * x5 + x4
  106. 0106exists b * x6 + 2 * x5
  107. 0107split
  108. 0108specialize pow_successor_compose (a)
  109. 0109specialize pow_successor_compose (S (S k))
  110. 0110specialize pow_successor_compose (x)
  111. 0111specialize pow_successor_compose (a * x)
  112. 0112apply pow_successor_compose
  113. 0113exact hprefix_witness_witness_witness_witness_witness_witness_witness_left
  114. 0114apply mul_comm
  115. 0115split
  116. 0116specialize pow_successor_compose (b)
  117. 0117specialize pow_successor_compose (S (S k))
  118. 0118specialize pow_successor_compose (x1)
  119. 0119specialize pow_successor_compose (b * x1)
  120. 0120apply pow_successor_compose
  121. 0121exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
  122. 0122apply mul_comm
  123. 0123split
  124. 0124exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_left
  125. 0125split
  126. 0126exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_left
  127. 0127split
  128. 0128rewrite hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  129. 0129specialize lte_natural_difference_successor (a)
  130. 0130specialize lte_natural_difference_successor (b)
  131. 0131specialize lte_natural_difference_successor (d)
  132. 0132specialize lte_natural_difference_successor (x1)
  133. 0133specialize lte_natural_difference_successor (x4)
  134. 0134apply lte_natural_difference_successor
  135. 0135exact ha
  136. 0136split
  137. 0137rewrite hB
  138. 0138rewrite hB
  139. 0139specialize lte_first_correction_successor (a)
  140. 0140specialize lte_first_correction_successor (b)
  141. 0141specialize lte_first_correction_successor (d)
  142. 0142specialize lte_first_correction_successor (S (S k))
  143. 0143specialize lte_first_correction_successor (x2)
  144. 0144specialize lte_first_correction_successor (x4)
  145. 0145specialize lte_first_correction_successor (x5)
  146. 0146apply lte_first_correction_successor
  147. 0147exact ha
  148. 0148exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  149. 0149rewrite hR
  150. 0150have hfirst : x4 = S (S k) * (b * x3) + d * x5
  151. 0151trans S (S k) * x2 + d * x5
  152. 0152exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_left
  153. 0153rewrite hR
  154. 0154refl
  155. 0155specialize lte_twice_correction_successor (b)
  156. 0156specialize lte_twice_correction_successor (d)
  157. 0157specialize lte_twice_correction_successor (S k)
  158. 0158specialize lte_twice_correction_successor (x3)
  159. 0159specialize lte_twice_correction_successor (x5)
  160. 0160specialize lte_twice_correction_successor (x4)
  161. 0161specialize lte_twice_correction_successor (x6)
  162. 0162apply lte_twice_correction_successor
  163. 0163exact hfirst
  164. 0164exact hprefix_witness_witness_witness_witness_witness_witness_witness_right_right_right_right_right_right