add_le_add_iff_right — Mathlib

English

For any a,b and natural n, a + n ≤ b + n if and only if a ≤ b.

Русский

Для любых ординалов a,b и натурального n: a + n ≤ b + n тогда и только тогда, когда a ≤ b.

LaTeX

$$$\forall a,b \in \mathrm{Ordinal}, \forall n \in \mathbb{N}, a+n \le b+n \iff a \le b$$$

Lean4

theorem add_le_add_iff_right {a b : Ordinal} : ∀ n : ℕ, a + n ≤ b + n ↔ a ≤ b
  | 0 => by simp
  | n + 1 => by simp only [natCast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right]

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