lean_workbook_plus_66512
ProvedProve that for all
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66512 (n k : ℕ) (h₁ : 1 ≤ k) (h₂ : k ≤ 2 * n) : k * (2 * n + 1 - k) ≤ n * (n + 1) := by sorry
Source
Prove that for all
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_66512 (n k : ℕ) (h₁ : 1 ≤ k) (h₂ : k ≤ 2 * n) : k * (2 * n + 1 - k) ≤ n * (n + 1) := by sorry