tsub_tsub_tsub_cancel_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

protected theorem tsub_tsub_tsub_cancel_left (hab : AddLECancellable (a - b)) (h : b ≤ a) : a - c - (a - b) = b - c :=
  by rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]

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