PA006N

division_block_upper

Stable checked-use theorem · independently closed

A bounded remainder keeps its decomposition below the next divisor block.

Exact expanded PA statement

forall d q r. (exists k. k + S r = d) -> exists k. k + S (d * q + r) = d * S q

Structural proof guide

Generated structural guide

A bounded remainder keeps its decomposition below the next divisor block.

Use the direct prerequisites add_assoc, add_comm as previously established PA formulas.

The proof proceeds by case analysis (1).

Referenced ingredients

PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm

Direct dependents

PA00DS nonzero_remainder_division_positive_multiple_threshold

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro d
  2. 0002intro q
  3. 0003intro r
  4. 0004intro h
  5. 0005cases h
  6. 0006exists x
  7. 0007trans S (x + (d * q + r))
  8. 0008apply PA4
  9. 0009trans S ((x + d * q) + r)
  10. 0010congr
  11. 0011symm
  12. 0012apply add_assoc
  13. 0013trans S ((d * q + x) + r)
  14. 0014congr
  15. 0015congr
  16. 0016apply add_comm
  17. 0017refl
  18. 0018trans S (d * q + (x + r))
  19. 0019congr
  20. 0020apply add_assoc
  21. 0021trans d * q + S (x + r)
  22. 0022symm
  23. 0023apply PA4
  24. 0024trans d * q + (x + S r)
  25. 0025congr
  26. 0026refl
  27. 0027symm
  28. 0028apply PA4
  29. 0029trans d * q + d
  30. 0030congr
  31. 0031refl
  32. 0032exact h_witness
  33. 0033symm
  34. 0034apply PA6