case inl
n k : ℕ
h : n < k
⊢ descFactorial n k = k ! * choose n k

case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = k ! * choose n k
n k : ℕ
⊢ descFactorial n k = k ! * choose n k
obtain h | h := Nat.lt_or_ge n k
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = choose n k * k !
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = k ! * choose n k
rw [mul_comm]
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k * (n - k)! = choose n k * k ! * (n - k)!
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k = choose n k * k !
apply mul_right_cancel₀ (factorial_ne_zero (n - k))
no goals
case inr
n k : ℕ
h : n ≥ k
⊢ descFactorial n k * (n - k)! = choose n k * k ! * (n - k)!
rw [choose_mul_factorial_mul_factorial h, ← factorial_mul_descFactorial h, mul_comm]
no goals
case inl
n k : ℕ
h : n < k
⊢ descFactorial n k = k ! * choose n k
rw [descFactorial_eq_zero_iff_lt.2 h, choose_eq_zero_of_lt h, mul_zero]