no goals
x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1
norm_num [centralBinom, choose]
no goals
x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2
norm_num [centralBinom, choose]
no goals
x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3
norm_num [centralBinom, choose]
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * ((n + 4) * centralBinom (n + 4))
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * (n + 4) * centralBinom (n + 4)
rw [mul_assoc]
no goals
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * ((n + 4) * centralBinom (n + 4))
refine' le_mul_of_pos_left zero_lt_two