no goals
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 0 → descFactorial n 0 < n ^ 0
rintro ⟨⟩
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ descFactorial n 1 < n ^ 1
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 1 → descFactorial n 1 < n ^ 1
intro
no goals
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ descFactorial n 1 < n ^ 1
contradiction
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 2) < n ^ (k + 2)
rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
no goals
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ)
  (pow_pos (Nat.lt_of_succ_le hn) _)