EL0002

lte_natural_difference_successor

A power-difference quotient advances by the actual recurrence a*Q+B.

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. ∀ B. ∀ Q. a = b + d → a · (B + d · Q) = b · B + d · (a · Q + B)

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

Definition DAG

none

Actual proof prerequisites

add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisitemul_comm · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitenatural_mul_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall a b d B Q. a = b + d -> a * (B + d * Q) = b * B + d * (a * Q + B)

Complete tactic proof in conservative notation

All 91 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

91 script commands · 22 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro d
  4. L4
    intro B
  5. L5
    intro Q
  6. L6
    intro ha
02Calculate and transport equalitiesL7–13

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

  1. L7
    rewrite ha
  2. L8
    rewrite ha
  3. L9
    trans ((((b) * (B))) + ((((b) * (((d) * (Q))))) + ((((d) * (B))) + (((d) * (((d) * (Q))))))))
  4. L10
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  5. L11
    trans ((((B) * (b))) + ((((Q) * (((b) * (d))))) + ((((B) * (d))) + (((Q) * (((d) * (d))))))))
  6. L12
    congr
  7. L13
    trans ((B) * (b))
03Use earlier factsL14–14

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

  1. L14
    apply mul_comm
04Calculate and transport equalitiesL15–22

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

  1. L15
    congr
  2. L16
    refl
  3. L17
    refl
  4. L18
    congr
  5. L19
    trans ((Q) * (((b) * (d))))
  6. L20
    trans ((b) * (((Q) * (d))))
  7. L21
    congr
  8. L22
    refl
05Use earlier factsL23–24

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

  1. L23
    apply mul_comm
  2. L24
    apply natural_mul_swap_right_tail
06Calculate and transport equalitiesL25–29

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

  1. L25
    congr
  2. L26
    refl
  3. L27
    refl
  4. L28
    congr
  5. L29
    trans ((B) * (d))
07Use earlier factsL30–30

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

  1. L30
    apply mul_comm
08Calculate and transport equalitiesL31–37

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

  1. L31
    congr
  2. L32
    refl
  3. L33
    refl
  4. L34
    trans ((Q) * (((d) * (d))))
  5. L35
    trans ((d) * (((Q) * (d))))
  6. L36
    congr
  7. L37
    refl
09Use earlier factsL38–39

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

  1. L38
    apply mul_comm
  2. L39
    apply natural_mul_swap_right_tail
10Calculate and transport equalitiesL40–48

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

  1. L40
    congr
  2. L41
    refl
  3. L42
    refl
  4. L43
    trans ((((B) * (b))) + ((((Q) * (((b) * (d))))) + ((((Q) * (((d) * (d))))) + (((B) * (d))))))
  5. L44
    congr
  6. L45
    refl
  7. L46
    congr
  8. L47
    refl
  9. L48
    trans ((((Q) * (((d) * (d))))) + (((B) * (d))))
11Use earlier factsL49–49

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

  1. L49
    apply add_comm
12Calculate and transport equalitiesL50–56

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

  1. L50
    congr
  2. L51
    refl
  3. L52
    refl
  4. L53
    trans ((((b) * (B))) + ((((d) * (((b) * (Q))))) + ((((d) * (((d) * (Q))))) + (((d) * (B))))))
  5. L54
    symm
  6. L55
    congr
  7. L56
    trans ((B) * (b))
13Use earlier factsL57–57

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

  1. L57
    apply mul_comm
14Calculate and transport equalitiesL58–65

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

  1. L58
    congr
  2. L59
    refl
  3. L60
    refl
  4. L61
    congr
  5. L62
    trans ((Q) * (((d) * (b))))
  6. L63
    trans ((d) * (((Q) * (b))))
  7. L64
    congr
  8. L65
    refl
15Use earlier factsL66–67

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

  1. L66
    apply mul_comm
  2. L67
    apply natural_mul_swap_right_tail
16Calculate and transport equalitiesL68–70

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

  1. L68
    congr
  2. L69
    refl
  3. L70
    trans ((b) * (d))
17Use earlier factsL71–71

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

  1. L71
    apply mul_comm
18Calculate and transport equalitiesL72–79

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

  1. L72
    congr
  2. L73
    refl
  3. L74
    refl
  4. L75
    congr
  5. L76
    trans ((Q) * (((d) * (d))))
  6. L77
    trans ((d) * (((Q) * (d))))
  7. L78
    congr
  8. L79
    refl
19Use earlier factsL80–81

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

  1. L80
    apply mul_comm
  2. L81
    apply natural_mul_swap_right_tail
20Calculate and transport equalitiesL82–85

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

  1. L82
    congr
  2. L83
    refl
  3. L84
    refl
  4. L85
    trans ((B) * (d))
21Use earlier factsL86–86

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

  1. L86
    apply mul_comm
22Calculate and transport equalitiesL87–91

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

  1. L87
    congr
  2. L88
    refl
  3. L89
    refl
  4. L90
    symm
  5. L91
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro d
  4. 0004intro B
  5. 0005intro Q
  6. 0006intro ha
  7. 0007rewrite ha
  8. 0008rewrite ha
  9. 0009trans ((((b) * (B))) + ((((b) * (((d) * (Q))))) + ((((d) * (B))) + (((d) * (((d) * (Q))))))))
  10. 0010simp [add_mul, mul_add, mul_assoc, add_assoc]
  11. 0011trans ((((B) * (b))) + ((((Q) * (((b) * (d))))) + ((((B) * (d))) + (((Q) * (((d) * (d))))))))
  12. 0012congr
  13. 0013trans ((B) * (b))
  14. 0014apply mul_comm
  15. 0015congr
  16. 0016refl
  17. 0017refl
  18. 0018congr
  19. 0019trans ((Q) * (((b) * (d))))
  20. 0020trans ((b) * (((Q) * (d))))
  21. 0021congr
  22. 0022refl
  23. 0023apply mul_comm
  24. 0024apply natural_mul_swap_right_tail
  25. 0025congr
  26. 0026refl
  27. 0027refl
  28. 0028congr
  29. 0029trans ((B) * (d))
  30. 0030apply mul_comm
  31. 0031congr
  32. 0032refl
  33. 0033refl
  34. 0034trans ((Q) * (((d) * (d))))
  35. 0035trans ((d) * (((Q) * (d))))
  36. 0036congr
  37. 0037refl
  38. 0038apply mul_comm
  39. 0039apply natural_mul_swap_right_tail
  40. 0040congr
  41. 0041refl
  42. 0042refl
  43. 0043trans ((((B) * (b))) + ((((Q) * (((b) * (d))))) + ((((Q) * (((d) * (d))))) + (((B) * (d))))))
  44. 0044congr
  45. 0045refl
  46. 0046congr
  47. 0047refl
  48. 0048trans ((((Q) * (((d) * (d))))) + (((B) * (d))))
  49. 0049apply add_comm
  50. 0050congr
  51. 0051refl
  52. 0052refl
  53. 0053trans ((((b) * (B))) + ((((d) * (((b) * (Q))))) + ((((d) * (((d) * (Q))))) + (((d) * (B))))))
  54. 0054symm
  55. 0055congr
  56. 0056trans ((B) * (b))
  57. 0057apply mul_comm
  58. 0058congr
  59. 0059refl
  60. 0060refl
  61. 0061congr
  62. 0062trans ((Q) * (((d) * (b))))
  63. 0063trans ((d) * (((Q) * (b))))
  64. 0064congr
  65. 0065refl
  66. 0066apply mul_comm
  67. 0067apply natural_mul_swap_right_tail
  68. 0068congr
  69. 0069refl
  70. 0070trans ((b) * (d))
  71. 0071apply mul_comm
  72. 0072congr
  73. 0073refl
  74. 0074refl
  75. 0075congr
  76. 0076trans ((Q) * (((d) * (d))))
  77. 0077trans ((d) * (((Q) * (d))))
  78. 0078congr
  79. 0079refl
  80. 0080apply mul_comm
  81. 0081apply natural_mul_swap_right_tail
  82. 0082congr
  83. 0083refl
  84. 0084refl
  85. 0085trans ((B) * (d))
  86. 0086apply mul_comm
  87. 0087congr
  88. 0088refl
  89. 0089refl
  90. 0090symm
  91. 0091simp [add_mul, mul_add, mul_assoc, add_assoc]