BT003T

mod_eq_mul_left

Stable · empty-context checked

Balanced congruence is preserved by multiplication on the left.

Exact expanded PA statement

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

Structural proof guide

Balanced congruence is preserved by multiplication on the left.

Direct prerequisites: mod_eq_mul_right, mul_comm. The authored body proceeds by case analysis (2), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT003S mod_eq_mul_right BT0006 mul_comm

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 h
  6. 0006specialize mod_eq_mul_right m
  7. 0007specialize mod_eq_mul_right a
  8. 0008specialize mod_eq_mul_right b
  9. 0009specialize mod_eq_mul_right c
  10. 0010have hr : exists r s. (a * c) + m * r = (b * c) + m * s
  11. 0011apply mod_eq_mul_right
  12. 0012exact h
  13. 0013cases hr
  14. 0014cases hr_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017trans a * c + m * x
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl
  21. 0021trans b * c + m * x1
  22. 0022exact hr_witness_witness
  23. 0023congr
  24. 0024apply mul_comm
  25. 0025refl