KU0000 · theorem body

division_add_quotient_bit

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

Adding arbitrary dividends changes the sum of their quotients by at most one carry.

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.

Statement with defined notation

∀ d. ∀ a. ∀ b. ∀ q. ∀ r. ∀ s. ∀ t. ∀ Q. ∀ R. DivRem(a,d,q,r) → DivRem(b,d,s,t) → DivRem(a + b,d,Q,R) → Q = q + s ∨ Q = S (q + s)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0007 DivRem

In local proof propositions

PD0002 Lt
Exact expanded first-order statement
forall d a b q r s t Q R. (((a) = (d) * (q) + (r) /\ (exists bcf_lt_gap_kmvadqb_left_bound. bcf_lt_gap_kmvadqb_left_bound + S (r) = d))) -> (((b) = (d) * (s) + (t) /\ (exists bcf_lt_gap_kmvadqb_right_bound. bcf_lt_gap_kmvadqb_right_bound + S (t) = d))) -> (((a + b) = (d) * (Q) + (R) /\ (exists bcf_lt_gap_kmvadqb_total_bound. bcf_lt_gap_kmvadqb_total_bound + S (R) = d))) -> (Q = q + s \/ Q = S (q + s))

Proof neighborhood

Direct theorem prerequisites

le_or_lt · Stable closed le_eq_or_lt · Stable closed lt_not_le · Stable closed zero_le · Stable closed one_le_of_ne_zero · Stable closed add_shuffle_middle · Alpha closed mul_add · Stable closed add_assoc · Stable closed add_comm · Stable closed add_lt_add · Alpha closed add_lt_cancel_left · Alpha closed division_remainder_unique · Stable closed

Direct theorem dependents

KU0001 division_add_quotient_lower KU0002 division_add_quotient_upper KU0006 add_quotient_carry_choice

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

138 script commands · 30 reading checkpoints · 12 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–10

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro q
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro t
  8. L8
    intro Q
  9. L9
    intro R
  10. L10
    intro hleft
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hright
  2. L12
    intro htotal
03Separate the logical casesL13–15

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

  1. L13
    cases hleft
  2. L14
    cases hright
  3. L15
    cases htotal
04Establish hsum_eqL16–25

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

  1. L16
    have hsum_eq : a + b = d * (q + s) + (r + t)
  2. L17
    rewrite hleft_left
  3. L18
    rewrite hright_left
  4. L19
    trans (d * q + d * s) + (r + t)
  5. L20
    apply add_shuffle_middle
  6. L21
    congr
  7. L22
    symm
  8. L23
    apply mul_add
  9. L24
    refl
  10. L25
    specialize le_or_lt (r + t)
05Use earlier factsL26–26

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

  1. L26
    specialize le_or_lt d
06Separate the logical casesL27–27

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

  1. L27
    cases le_or_lt
07Establish hsplitL28–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L28
    have hsplit : r + t = d ∨ Lt(r + t,d)Definitions: Lt(r + t,d)Original native command in the exact edition
  2. L29
    specialize le_eq_or_lt (r + t)
  3. L30
    specialize le_eq_or_lt d
  4. L31
    apply le_eq_or_lt
  5. L32
    exact le_or_lt_left
08Separate the logical casesL33–33

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

  1. L33
    cases hsplit
09Establish hd0L34–42

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

  1. L34
    have hd0 : ~(d = 0)
  2. L35
    intro hd
  3. L36
    rewrite hd at hleft_right
  4. L37
    specialize lt_not_le r
  5. L38
    specialize lt_not_le 0
  6. L39
    apply lt_not_le
  7. L40
    exact hleft_right
  8. L41
    specialize zero_le r
  9. L42
    exact zero_le
10Establish hzero_boundL43–46

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

  1. L43
    have hzero_bound : Lt(0,d)Definitions: Lt(0,d)Original native command in the exact edition
  2. L44
    specialize one_le_of_ne_zero d
  3. L45
    apply one_le_of_ne_zero
  4. L46
    exact hd0
11Establish hcandidate_eqL47–55

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

  1. L47
    have hcandidate_eq : a + b = d * S (q + s) + 0
  2. L48
    trans d * (q + s) + (r + t)
  3. L49
    exact hsum_eq
  4. L50
    rewrite hsplit_left
  5. L51
    trans d * S (q + s)
  6. L52
    symm
  7. L53
    apply PA6
  8. L54
    symm
  9. L55
    apply PA3
12Establish huniqueL56–65

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

  1. L56
    have hunique : Q = S (q + s) /\ R = 0
  2. L57
    specialize division_remainder_unique d
  3. L58
    specialize division_remainder_unique (a + b)
  4. L59
    specialize division_remainder_unique Q
  5. L60
    specialize division_remainder_unique R
  6. L61
    specialize division_remainder_unique (S (q + s))
  7. L62
    specialize division_remainder_unique 0
  8. L63
    apply division_remainder_unique
  9. L64
    exact htotal_left
  10. L65
    exact htotal_right
13Use earlier factsL66–67

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

  1. L66
    exact hcandidate_eq
  2. L67
    exact hzero_bound
14Separate the logical casesL68–69

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

  1. L68
    cases hunique
  2. L69
    right
15Use earlier factsL70–70

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

  1. L70
    exact hunique_left
16Establish huniqueL71–80

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

  1. L71
    have hunique : Q = q + s /\ R = r + t
  2. L72
    specialize division_remainder_unique d
  3. L73
    specialize division_remainder_unique (a + b)
  4. L74
    specialize division_remainder_unique Q
  5. L75
    specialize division_remainder_unique R
  6. L76
    specialize division_remainder_unique (q + s)
  7. L77
    specialize division_remainder_unique (r + t)
  8. L78
    apply division_remainder_unique
  9. L79
    exact htotal_left
  10. L80
    exact htotal_right
17Use earlier factsL81–82

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

  1. L81
    exact hsum_eq
  2. L82
    exact hsplit_right
18Separate the logical casesL83–84

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

  1. L83
    cases hunique
  2. L84
    left
19Use earlier factsL85–85

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

  1. L85
    exact hunique_left
20Separate the logical casesL86–86

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

  1. L86
    cases le_or_lt_right
21Establish hremaindersL87–96

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

  1. L87
    have hremainders : r + t = d + S x
  2. L88
    trans x + S d
  3. L89
    symm
  4. L90
    exact le_or_lt_right_witness
  5. L91
    trans S (x + d)
  6. L92
    apply PA4
  7. L93
    trans S (d + x)
  8. L94
    congr
  9. L95
    apply add_comm
  10. L96
    symm
22Use earlier factsL97–97

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

  1. L97
    apply PA4
23Establish hsum_ltL98–106

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

  1. L98
    have hsum_lt : Lt(r + t,d + d)Definitions: Lt(r + t,d + d)Original native command in the exact edition
  2. L99
    specialize add_lt_add r
  3. L100
    specialize add_lt_add d
  4. L101
    specialize add_lt_add t
  5. L102
    specialize add_lt_add d
  6. L103
    apply add_lt_add
  7. L104
    exact hleft_right
  8. L105
    exact hright_right
  9. L106
    rewrite hremainders at hsum_lt
24Establish hcarry_boundL107–112

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add lt cancel left.

  1. L107
    have hcarry_bound : Lt(S x,d)Definitions: Lt(S x,d)Original native command in the exact edition
  2. L108
    specialize add_lt_cancel_left d
  3. L109
    specialize add_lt_cancel_left (S x)
  4. L110
    specialize add_lt_cancel_left d
  5. L111
    apply add_lt_cancel_left
  6. L112
    exact hsum_lt
25Establish hcandidate_eqL113–122

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

  1. L113
    have hcandidate_eq : a + b = d * S (q + s) + S x
  2. L114
    trans d * (q + s) + (r + t)
  3. L115
    exact hsum_eq
  4. L116
    rewrite hremainders
  5. L117
    trans (d * (q + s) + d) + S x
  6. L118
    symm
  7. L119
    apply add_assoc
  8. L120
    congr
  9. L121
    symm
  10. L122
    apply PA6
26Calculate and transport equalitiesL123–123

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

  1. L123
    refl
27Establish huniqueL124–133

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

  1. L124
    have hunique : Q = S (q + s) /\ R = S x
  2. L125
    specialize division_remainder_unique d
  3. L126
    specialize division_remainder_unique (a + b)
  4. L127
    specialize division_remainder_unique Q
  5. L128
    specialize division_remainder_unique R
  6. L129
    specialize division_remainder_unique (S (q + s))
  7. L130
    specialize division_remainder_unique (S x)
  8. L131
    apply division_remainder_unique
  9. L132
    exact htotal_left
  10. L133
    exact htotal_right
28Use earlier factsL134–135

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

  1. L134
    exact hcandidate_eq
  2. L135
    exact hcarry_bound
29Separate the logical casesL136–137

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

  1. L136
    cases hunique
  2. L137
    right
30Use earlier factsL138–138

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

  1. L138
    exact hunique_left

Library-wide reading audit

Original defined command ledger · 138 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro q
  5. 0005intro r
  6. 0006intro s
  7. 0007intro t
  8. 0008intro Q
  9. 0009intro R
  10. 0010intro hleft
  11. 0011intro hright
  12. 0012intro htotal
  13. 0013cases hleft
  14. 0014cases hright
  15. 0015cases htotal
  16. 0016have hsum_eq : a + b = d * (q + s) + (r + t)
  17. 0017rewrite hleft_left
  18. 0018rewrite hright_left
  19. 0019trans (d * q + d * s) + (r + t)
  20. 0020apply add_shuffle_middle
  21. 0021congr
  22. 0022symm
  23. 0023apply mul_add
  24. 0024refl
  25. 0025specialize le_or_lt (r + t)
  26. 0026specialize le_or_lt d
  27. 0027cases le_or_lt
  28. 0028have hsplit : r + t = d ∨ Lt(r + t,d)
    Exact native replay linehave hsplit : r + t = d \/ exists z. z + S (r + t) = d
  29. 0029specialize le_eq_or_lt (r + t)
  30. 0030specialize le_eq_or_lt d
  31. 0031apply le_eq_or_lt
  32. 0032exact le_or_lt_left
  33. 0033cases hsplit
  34. 0034have hd0 : ~(d = 0)
  35. 0035intro hd
  36. 0036rewrite hd at hleft_right
  37. 0037specialize lt_not_le r
  38. 0038specialize lt_not_le 0
  39. 0039apply lt_not_le
  40. 0040exact hleft_right
  41. 0041specialize zero_le r
  42. 0042exact zero_le
  43. 0043have hzero_bound : Lt(0,d)
    Exact native replay linehave hzero_bound : exists z. z + S 0 = d
  44. 0044specialize one_le_of_ne_zero d
  45. 0045apply one_le_of_ne_zero
  46. 0046exact hd0
  47. 0047have hcandidate_eq : a + b = d * S (q + s) + 0
  48. 0048trans d * (q + s) + (r + t)
  49. 0049exact hsum_eq
  50. 0050rewrite hsplit_left
  51. 0051trans d * S (q + s)
  52. 0052symm
  53. 0053apply PA6
  54. 0054symm
  55. 0055apply PA3
  56. 0056have hunique : Q = S (q + s) /\ R = 0
  57. 0057specialize division_remainder_unique d
  58. 0058specialize division_remainder_unique (a + b)
  59. 0059specialize division_remainder_unique Q
  60. 0060specialize division_remainder_unique R
  61. 0061specialize division_remainder_unique (S (q + s))
  62. 0062specialize division_remainder_unique 0
  63. 0063apply division_remainder_unique
  64. 0064exact htotal_left
  65. 0065exact htotal_right
  66. 0066exact hcandidate_eq
  67. 0067exact hzero_bound
  68. 0068cases hunique
  69. 0069right
  70. 0070exact hunique_left
  71. 0071have hunique : Q = q + s /\ R = r + t
  72. 0072specialize division_remainder_unique d
  73. 0073specialize division_remainder_unique (a + b)
  74. 0074specialize division_remainder_unique Q
  75. 0075specialize division_remainder_unique R
  76. 0076specialize division_remainder_unique (q + s)
  77. 0077specialize division_remainder_unique (r + t)
  78. 0078apply division_remainder_unique
  79. 0079exact htotal_left
  80. 0080exact htotal_right
  81. 0081exact hsum_eq
  82. 0082exact hsplit_right
  83. 0083cases hunique
  84. 0084left
  85. 0085exact hunique_left
  86. 0086cases le_or_lt_right
  87. 0087have hremainders : r + t = d + S x
  88. 0088trans x + S d
  89. 0089symm
  90. 0090exact le_or_lt_right_witness
  91. 0091trans S (x + d)
  92. 0092apply PA4
  93. 0093trans S (d + x)
  94. 0094congr
  95. 0095apply add_comm
  96. 0096symm
  97. 0097apply PA4
  98. 0098have hsum_lt : Lt(r + t,d + d)
    Exact native replay linehave hsum_lt : exists z. z + S (r + t) = d + d
  99. 0099specialize add_lt_add r
  100. 0100specialize add_lt_add d
  101. 0101specialize add_lt_add t
  102. 0102specialize add_lt_add d
  103. 0103apply add_lt_add
  104. 0104exact hleft_right
  105. 0105exact hright_right
  106. 0106rewrite hremainders at hsum_lt
  107. 0107have hcarry_bound : Lt(S x,d)
    Exact native replay linehave hcarry_bound : exists z. z + S (S x) = d
  108. 0108specialize add_lt_cancel_left d
  109. 0109specialize add_lt_cancel_left (S x)
  110. 0110specialize add_lt_cancel_left d
  111. 0111apply add_lt_cancel_left
  112. 0112exact hsum_lt
  113. 0113have hcandidate_eq : a + b = d * S (q + s) + S x
  114. 0114trans d * (q + s) + (r + t)
  115. 0115exact hsum_eq
  116. 0116rewrite hremainders
  117. 0117trans (d * (q + s) + d) + S x
  118. 0118symm
  119. 0119apply add_assoc
  120. 0120congr
  121. 0121symm
  122. 0122apply PA6
  123. 0123refl
  124. 0124have hunique : Q = S (q + s) /\ R = S x
  125. 0125specialize division_remainder_unique d
  126. 0126specialize division_remainder_unique (a + b)
  127. 0127specialize division_remainder_unique Q
  128. 0128specialize division_remainder_unique R
  129. 0129specialize division_remainder_unique (S (q + s))
  130. 0130specialize division_remainder_unique (S x)
  131. 0131apply division_remainder_unique
  132. 0132exact htotal_left
  133. 0133exact htotal_right
  134. 0134exact hcandidate_eq
  135. 0135exact hcarry_bound
  136. 0136cases hunique
  137. 0137right
  138. 0138exact hunique_left