BT003R

mod_eq_add

Stable · empty-context checked

Balanced natural congruence respects addition.

Exact expanded PA statement

forall m a b c d. (exists u v. a + m * u = b + m * v) -> (exists r s. c + m * r = d + m * s) -> exists x y. (a + c) + m * x = (b + d) + m * y

Structural proof guide

Balanced natural congruence respects addition.

Direct prerequisites: mul_add, add_comm, add_permute_outer. The authored body proceeds by case analysis (4).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0002 add_comm BT0032 add_permute_outer

Direct dependents

BT004F binary_crt

Formal native tactic body

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

  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro hab
  7. 0007intro hcd
  8. 0008cases hab
  9. 0009cases hab_witness
  10. 0010cases hcd
  11. 0011cases hcd_witness
  12. 0012exists x2 + x
  13. 0013exists x3 + x1
  14. 0014trans (a + c) + (m * x2 + m * x)
  15. 0015congr
  16. 0016refl
  17. 0017apply mul_add
  18. 0018trans (m * x2 + c) + (a + m * x)
  19. 0019apply add_permute_outer
  20. 0020trans (c + m * x2) + (a + m * x)
  21. 0021congr
  22. 0022apply add_comm
  23. 0023refl
  24. 0024trans (a + m * x) + (c + m * x2)
  25. 0025apply add_comm
  26. 0026trans (b + m * x1) + (d + m * x3)
  27. 0027congr
  28. 0028exact hab_witness_witness
  29. 0029exact hcd_witness_witness
  30. 0030trans (d + m * x3) + (b + m * x1)
  31. 0031apply add_comm
  32. 0032trans (m * x3 + d) + (b + m * x1)
  33. 0033congr
  34. 0034apply add_comm
  35. 0035refl
  36. 0036trans (b + d) + (m * x3 + m * x1)
  37. 0037symm
  38. 0038apply add_permute_outer
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add