no goals
n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ descFactorial n 0
rw [descFactorial_zero, pow_zero]
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * descFactorial n k
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ descFactorial n (k + 1)
rw [descFactorial_succ, pow_succ, succ_sub_succ, mul_comm]
case h₁
n k : ℕ
⊢ (n - k) ^ k ≤ descFactorial n k
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * descFactorial n k
apply Nat.mul_le_mul_of_nonneg_left
no goals
case h₁
n k : ℕ
⊢ (n - k) ^ k ≤ descFactorial n k
exact   (le_trans (Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ _) _) k)
      (pow_sub_le_descFactorial n k))