tsub_eq_of_eq_add' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Weaker version of `AddLECancellable.tsub_eq_of_eq_add` assuming that `a = c + b` itself is
cancellable rather than `b`. -/
protected theorem tsub_eq_of_eq_add' [AddLeftMono α] (ha : AddLECancellable a) (h : a = c + b) : a - b = c :=
  (h ▸ ha).of_add_right.tsub_eq_of_eq_add h

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