no goals
n : ℕ
⊢ (n + 1 - 0) * descFactorial (n + 1) 0 = (n + 1) * descFactorial n 0
rw [tsub_zero, descFactorial_zero, descFactorial_zero]
no goals
n k : ℕ
⊢ (n + 1 - (k + 1)) * descFactorial (n + 1) (k + 1) = (n + 1) * descFactorial n (k + 1)
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]