sub_sub_sub_cancel_left — Mathlib

English

If a ≠ ∞ and b ≤ a, then a − c − (a − b) = b − c for all c.

Русский

Если a ≠ ∞ и b ≤ a, то для любого c выполняется a − c − (a − b) = b − c.

LaTeX

$$$ (ha : a \neq \infty) (h : b \le a) \Rightarrow a - c - (a - b) = b - c $$$

Lean4

theorem sub_sub_sub_cancel_left (ha : a ≠ ∞) (h : b ≤ a) : a - c - (a - b) = b - c :=
  by
  have hb : b ≠ ∞ := ne_top_of_le_ne_top ha h
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  cases c
  · simp
  · norm_cast
    rw [tsub_tsub_tsub_cancel_left]
    exact mod_cast h

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