no goals
n : ℕ
⊢ descFactorial (n + 0) 0 = ascFactorial n 0
rw [ascFactorial_zero, descFactorial_zero]
no goals
n k : ℕ
⊢ descFactorial (n + succ k) (succ k) = ascFactorial n (succ k)
rw [Nat.add_succ, Nat.succ_eq_add_one, Nat.succ_eq_add_one,
    succ_descFactorial_succ, ascFactorial_succ, add_descFactorial_eq_ascFactorial _ k]