BT003Q

mod_eq_trans

Stable · empty-context checked

Balanced natural congruence is transitive.

Exact expanded PA statement

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

Structural proof guide

Balanced natural congruence is transitive.

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

Proof neighborhood

Direct dependencies

BT0003 add_assoc BT0002 add_comm BT0007 mul_add

Direct dependents

BT003X mod_eq_to_remainder_decomposition BT004F binary_crt BT004U binary_crt_fold_step

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 hab
  6. 0006intro hbc
  7. 0007cases hab
  8. 0008cases hab_witness
  9. 0009cases hbc
  10. 0010cases hbc_witness
  11. 0011exists x + x2
  12. 0012exists x3 + x1
  13. 0013trans a + (m * x + m * x2)
  14. 0014congr
  15. 0015refl
  16. 0016apply mul_add
  17. 0017trans (a + m * x) + m * x2
  18. 0018symm
  19. 0019apply add_assoc
  20. 0020trans (b + m * x1) + m * x2
  21. 0021congr
  22. 0022exact hab_witness_witness
  23. 0023refl
  24. 0024trans b + (m * x1 + m * x2)
  25. 0025apply add_assoc
  26. 0026trans b + (m * x2 + m * x1)
  27. 0027congr
  28. 0028refl
  29. 0029apply add_comm
  30. 0030trans (b + m * x2) + m * x1
  31. 0031symm
  32. 0032apply add_assoc
  33. 0033trans (c + m * x3) + m * x1
  34. 0034congr
  35. 0035exact hbc_witness_witness
  36. 0036refl
  37. 0037trans c + (m * x3 + m * x1)
  38. 0038apply add_assoc
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add