n : ℕ
this : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
n : ℕ
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
have : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact n.succ_ne_zero
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
n : ℕ
this : ↑n + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
have : (n : ℚ) + 1 + 1 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
have h : (n : ℚ) + 2 ≠ 0 := by norm_cast; exact (n + 1).succ_ne_zero
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ ↑(Nat.centralBinom (n + 1)) * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑1 * ↑(Nat.centralBinom (n + 1)) * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ gosperCatalan (n + 1) (n + 1) - gosperCatalan (n + 1) 0 = ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
simp only [gosperCatalan, Nat.sub_zero, Nat.centralBinom_zero, Nat.sub_self]
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ (↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) - (↑n + 1)) - ↑(Nat.centralBinom (n + 1)) * (-1 + -↑n)) * (↑n + 2) =
    ↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) * (↑n + 1 + 1))
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ ↑(Nat.centralBinom (n + 1)) * ↑1 * (2 * ↑(n + 1) - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) -
      ↑1 * ↑(Nat.centralBinom (n + 1)) * (2 * ↑0 - ↑(n + 1)) / (2 * ↑(n + 1) * (↑(n + 1) + 1)) =
    ↑(Nat.centralBinom (n + 1)) / (↑n + 2)
field_simp
no goals
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
h : ↑n + 2 ≠ 0
⊢ (↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) - (↑n + 1)) - ↑(Nat.centralBinom (n + 1)) * (-1 + -↑n)) * (↑n + 2) =
    ↑(Nat.centralBinom (n + 1)) * (2 * (↑n + 1) * (↑n + 1 + 1))
ring
n : ℕ
⊢ ¬n + 1 = 0
n : ℕ
⊢ ↑n + 1 ≠ 0
norm_cast
no goals
n : ℕ
⊢ ¬n + 1 = 0
exact n.succ_ne_zero
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ↑n + 1 + 1 ≠ 0
norm_cast
no goals
n : ℕ
this : ↑n + 1 ≠ 0
⊢ ¬n + 1 + 1 = 0
exact (n + 1).succ_ne_zero
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ¬n + 2 = 0
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ↑n + 2 ≠ 0
norm_cast
no goals
n : ℕ
this✝ : ↑n + 1 ≠ 0
this : ↑n + 1 + 1 ≠ 0
⊢ ¬n + 2 = 0
exact (n + 1).succ_ne_zero