lean_workbook_plus_17363
ProvedShow that for and , .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17363 (n k : ℕ) (h₁ : 1 ≤ k ∧ k ≤ n) : k * (n - k + 1) ≥ n := by sorry
Source
Show that for and , .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_17363 (n k : ℕ) (h₁ : 1 ≤ k ∧ k ≤ n) : k * (n - k + 1) ≥ n := by sorry