BT011C

scaled_remainder_lift

Alpha body-checked · checked-use disabled

Scale a quotient-remainder equation and normalize its new tail.

Exact expanded PA statement

forall d x q t c r s u. x = d * q + t -> c * t + r = d * s + u -> c * x + r = d * (c * q + s) + u

Structural proof guide

Scale a quotient-remainder equation and normalize its new tail.

Direct prerequisites: mul_add, mul_assoc, mul_comm, add_assoc. The authored body proceeds by intermediate claims (4), equality transport (6).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT0003 add_assoc

Direct dependents

BT011E double_scaled_remainder_lift BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro d
  2. 0002intro x
  3. 0003intro q
  4. 0004intro t
  5. 0005intro c
  6. 0006intro r
  7. 0007intro s
  8. 0008intro u
  9. 0009intro hx
  10. 0010intro htail
  11. 0011rewrite hx
  12. 0012have hdist : c * (d * q + t) = c * (d * q) + c * t
  13. 0013specialize mul_add c
  14. 0014specialize mul_add (d * q)
  15. 0015specialize mul_add t
  16. 0016exact mul_add
  17. 0017rewrite hdist
  18. 0018have hassoc : (c * (d * q) + c * t) + r = c * (d * q) + (c * t + r)
  19. 0019apply add_assoc
  20. 0020rewrite hassoc
  21. 0021rewrite htail
  22. 0022have hfront : c * (d * q) = d * (c * q)
  23. 0023trans (c * d) * q
  24. 0024symm
  25. 0025apply mul_assoc
  26. 0026trans (d * c) * q
  27. 0027congr
  28. 0028apply mul_comm
  29. 0029refl
  30. 0030apply mul_assoc
  31. 0031rewrite hfront
  32. 0032have hdist2 : d * (c * q + s) = d * (c * q) + d * s
  33. 0033specialize mul_add d
  34. 0034specialize mul_add (c * q)
  35. 0035specialize mul_add s
  36. 0036exact mul_add
  37. 0037rewrite hdist2
  38. 0038symm
  39. 0039apply add_assoc