no goals
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(ascFactorial a b) = Polynomial.eval (↑a + 1) (pochhammer S b)
rw [← pochhammer_nat_eq_ascFactorial, pochhammer_eval_cast, Nat.cast_add, Nat.cast_one]