no goals
n : ℕ
⊢ n ! * ascFactorial n 0 = (n + 0)!
rw [ascFactorial, add_zero, mul_one]
no goals
n k : ℕ
⊢ n ! * ascFactorial n (k + 1) = (n + (k + 1))!
rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n k,
  ← add_assoc, ← Nat.succ_eq_add_one (n + k), factorial]