S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (pochhammer S 2) = ↑a * (↑a - 1)
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ ↑(descFactorial a 2) = ↑a * (↑a - 1)
rw [cast_descFactorial]
case zero
S : Type u_1
inst✝ : Ring S
b : ℕ
⊢ Polynomial.eval (↑(zero - (2 - 1))) (pochhammer S 2) = ↑zero * (↑zero - 1)

case succ
S : Type u_1
inst✝ : Ring S
b n✝ : ℕ
⊢ Polynomial.eval (↑(succ n✝ - (2 - 1))) (pochhammer S 2) = ↑(succ n✝) * (↑(succ n✝) - 1)
S : Type u_1
inst✝ : Ring S
a b : ℕ
⊢ Polynomial.eval (↑(a - (2 - 1))) (pochhammer S 2) = ↑a * (↑a - 1)
cases a
no goals
case zero
S : Type u_1
inst✝ : Ring S
b : ℕ
⊢ Polynomial.eval (↑(zero - (2 - 1))) (pochhammer S 2) = ↑zero * (↑zero - 1)
simp
no goals
case succ
S : Type u_1
inst✝ : Ring S
b n✝ : ℕ
⊢ Polynomial.eval (↑(succ n✝ - (2 - 1))) (pochhammer S 2) = ↑(succ n✝) * (↑(succ n✝) - 1)
rw [succ_sub_succ, tsub_zero, cast_succ, add_sub_cancel, pochhammer_succ_right, pochhammer_one,
  Polynomial.X_mul, Polynomial.eval_mul_X, Polynomial.eval_add, Polynomial.eval_X, cast_one,
  Polynomial.eval_one]