English
(n+1)·centralBinom(n+1) = 2(2n+1)·centralBinom(n).
Русский
(n+1)·centralBinom(n+1) = 2(2n+1)·centralBinom(n).
LaTeX
$$$$ (n+1) \\cdot \\binom{2(n+1)}{n+1} = 2(2n+1) \\cdot \\binom{2n}{n}. $$$$
Lean4
/-- An inductive property of the central binomial coefficient.
-/
theorem succ_mul_centralBinom_succ (n : ℕ) : (n + 1) * centralBinom (n + 1) = 2 * (2 * n + 1) * centralBinom n :=
calc
(n + 1) * (2 * (n + 1)).choose (n + 1) = (2 * n + 2).choose (n + 1) * (n + 1) := mul_comm _ _
_ = (2 * n + 1).choose n * (2 * n + 2) := by rw [choose_succ_right_eq, choose_mul_succ_eq]
_ = 2 * ((2 * n + 1).choose n * (n + 1)) := by ring
_ = 2 * ((2 * n + 1).choose n * (2 * n + 1 - n)) := by rw [two_mul n, add_assoc, Nat.add_sub_cancel_left]
_ = 2 * ((2 * n).choose n * (2 * n + 1)) := by rw [choose_mul_succ_eq]
_ = 2 * (2 * n + 1) * (2 * n).choose n := by rw [mul_assoc, mul_comm (2 * n + 1)]
