tsub_eq_of_eq_add_rev' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add_rev` assuming that `a = b + c` itself is
cancellable rather than `b`. -/
protected theorem tsub_eq_of_eq_add_rev' [AddLeftMono α] (ha : AddLECancellable a) (h : a = b + c) : a - b = c :=
  ha.tsub_eq_of_eq_add' <| by rw [add_comm, h]

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