lean_workbook_plus_22580
Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
For any m<n , (m+1n)=m+1n−m(mn) , so (m+1n)<(mn) if m<2n−1 and (m+1n)>(mn) if m>2n−1.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22580 (n m : ℕ) (h₁ : m < n) (h₂ : m < (n - 1) / 2) :
(n.choose (m + 1)) < (n.choose m) := by sorry
View graph