eq_tsub_of_add_eq — Mathlib

English

If c is cancellable and a + c = b, then a = b − c.

Русский

Если c является отменяемым и a + c = b, тогда a = b − c.

LaTeX

$$$ AddLECancellable(c) \land a + c = b \Rightarrow a = b - c $$$

Lean4

/-- See `AddLECancellable.eq_tsub_of_add_eq'` for a version assuming that `b = a + c` itself is
cancellable rather than `c`. -/
protected theorem eq_tsub_of_add_eq (hc : AddLECancellable c) (h : a + c = b) : a = b - c :=
  (hc.tsub_eq_of_eq_add h.symm).symm

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