no goals
n : ℕ
⊢ (n + 1) * ascFactorial (succ n) 0 = (n + 0 + 1) * ascFactorial n 0
rw [add_zero, ascFactorial_zero, ascFactorial_zero]
no goals
n k : ℕ
⊢ (n + 1) * ascFactorial (succ n) (k + 1) = (n + (k + 1) + 1) * ascFactorial n (k + 1)
rw [ascFactorial, mul_left_comm, succ_ascFactorial n k, ascFactorial,
  succ_add, ← add_assoc, succ_eq_add_one]