BT003S

mod_eq_mul_right

Stable · empty-context checked

Balanced congruence is preserved by multiplication on the right.

Exact expanded PA statement

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

Structural proof guide

Balanced congruence is preserved by multiplication on the right.

Direct prerequisites: add_mul, mul_assoc. The authored body proceeds by case analysis (2).

Proof neighborhood

Direct dependencies

BT000B add_mul BT0008 mul_assoc

Direct dependents

BT003T mod_eq_mul_left

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. 0006cases h
  7. 0007cases h_witness
  8. 0008exists x * c
  9. 0009exists x1 * c
  10. 0010trans a * c + (m * x) * c
  11. 0011congr
  12. 0012refl
  13. 0013symm
  14. 0014apply mul_assoc
  15. 0015trans (a + m * x) * c
  16. 0016symm
  17. 0017apply add_mul
  18. 0018trans (b + m * x1) * c
  19. 0019congr
  20. 0020exact h_witness_witness
  21. 0021refl
  22. 0022trans b * c + (m * x1) * c
  23. 0023apply add_mul
  24. 0024congr
  25. 0025refl
  26. 0026apply mul_assoc