choose_le_succ_of_lt_half_left — Mathlib

English

If r < n/2, then C(n,r) ≤ C(n,r+1).

Русский

Если r < n/2, то C(n,r) ≤ C(n,r+1).

LaTeX

$$$$ r < \frac{n}{2} \Rightarrow \binom{n}{r} \le \binom{n}{r+1} $$$$

Lean4

/-- Show that `Nat.choose` is increasing for small values of the right argument. -/
theorem choose_le_succ_of_lt_half_left {r n : ℕ} (h : r < n / 2) : choose n r ≤ choose n (r + 1) :=
  by
  refine Nat.le_of_mul_le_mul_right ?_ (Nat.sub_pos_of_lt (h.trans_le (n.div_le_self 2)))
  rw [← choose_succ_right_eq]
  apply Nat.mul_le_mul_left
  rw [← Nat.lt_iff_add_one_le, Nat.lt_sub_iff_add_lt, ← Nat.mul_two]
  exact lt_of_lt_of_le (Nat.mul_lt_mul_of_pos_right h Nat.zero_lt_two) (n.div_mul_le_self 2)

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