r n : ℕ
h : r < n / 2
⊢ choose n r * (n - r) ≤ choose n (r + 1) * (n - r)
r n : ℕ
h : r < n / 2
⊢ choose n r ≤ choose n (r + 1)
refine' le_of_mul_le_mul_right _ (lt_tsub_iff_left.mpr (lt_of_lt_of_le h (n.div_le_self 2)))
r n : ℕ
h : r < n / 2
⊢ choose n (r + 1) * (r + 1) ≤ choose n (r + 1) * (n - r)
r n : ℕ
h : r < n / 2
⊢ choose n r * (n - r) ≤ choose n (r + 1) * (n - r)
rw [← choose_succ_right_eq]
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
r n : ℕ
h : r < n / 2
⊢ choose n (r + 1) * (r + 1) ≤ choose n (r + 1) * (n - r)
apply Nat.mul_le_mul_left
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
case h
r n : ℕ
h : r < n / 2
⊢ r + 1 ≤ n - r
rw [← Nat.lt_iff_add_one_le, lt_tsub_iff_left, ← mul_two]
no goals
case h
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
exact lt_of_lt_of_le (mul_lt_mul_of_pos_right h zero_lt_two) (n.div_mul_le_self 2)