no goals
n : ℕ
⊢ descFactorial n 0 ≤ n ^ 0
rw [descFactorial_zero, pow_zero]
n k : ℕ
⊢ (n - k) * descFactorial n k ≤ n * n ^ k
n k : ℕ
⊢ descFactorial n (k + 1) ≤ n ^ (k + 1)
rw [descFactorial_succ, pow_succ, mul_comm _ n]
no goals
n k : ℕ
⊢ (n - k) * descFactorial n k ≤ n * n ^ k
exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)