no goals
n : ℕ
⊢ descFactorial (n + 1) (0 + 1) = (n + 1) * descFactorial n 0
rw [descFactorial_zero, descFactorial_one, mul_one]
no goals
n k : ℕ
⊢ descFactorial (n + 1) (succ k + 1) = (n + 1) * descFactorial n (succ k)
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
  mul_left_comm]