max_sq_add_min_le_pair — Mathlib

English

max(m,n)^2 + min(m,n) ≤ pair(m,n).

Русский

max(m,n)^2 + min(m,n) ≤ pair(m,n).

LaTeX

$$$ \max(m,n)^2 + \min(m,n) \le \operatorname{pair}(m,n). $$$

Lean4

theorem max_sq_add_min_le_pair (m n : ℕ) : max m n ^ 2 + min m n ≤ pair m n :=
  by
  rw [pair]
  rcases lt_or_ge m n with h | h
  · rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
  rw [if_neg h.not_gt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc, Nat.add_le_add_iff_left]
  exact Nat.le_add_left _ _

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