no goals
n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! * descFactorial n 0 = n !
rw [descFactorial_zero, mul_one, tsub_zero]
case h
k : ℕ
h : succ k ≤ 0
⊢ False
k : ℕ
h : succ k ≤ 0
⊢ (0 - succ k)! * descFactorial 0 (succ k) = 0!
exfalso
no goals
case h
k : ℕ
h : succ k ≤ 0
⊢ False
exact not_succ_le_zero k h
no goals
n k : ℕ
h : succ k ≤ succ n
⊢ (succ n - succ k)! * descFactorial (succ n) (succ k) = (succ n)!
rw [succ_descFactorial_succ, succ_sub_succ, ← mul_assoc, mul_comm (n - k)!, mul_assoc,
  factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]