add_tsub_tsub_cancel — Mathlib

English

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

Русский

Если a − c канцелируемо и c ≤ a, то a + b − (a − c) = b + c.

LaTeX

$$$ \forall a,b,c \in \alpha,\; AddLECancellable(a - c) \land c \le a \Rightarrow a + b - (a - c) = b + c $$$

Lean4

@[simp]
protected theorem add_tsub_tsub_cancel (hac : AddLECancellable (a - c)) (h : c ≤ a) : a + b - (a - c) = b + c :=
  hac.tsub_eq_of_eq_add <| by rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

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