tsub_eq_tsub_of_add_eq_add — Mathlib

English

If a + d = c + b, then a − b = c − d.

Русский

Если a + d = c + b, то a − b = c − d.

LaTeX

$$$ a + d = c + b \Rightarrow a - b = c - d $$$

Lean4

/-- A more general version of the reverse direction of `sub_eq_sub_iff_add_eq_add` -/
theorem tsub_eq_tsub_of_add_eq_add (h : a + d = c + b) : a - b = c - d := by
  calc
    a - b = a + d - d - b := by rw [add_tsub_cancel_right]
    _ = c + b - b - d := by rw [h, tsub_right_comm]
    _ = c - d := by rw [add_tsub_cancel_right]

Похожие утверждения