English
For n with k+2 ≤ n, we have (n−(k+1))^(k+2) < n.descFactorial(k+2).
Русский
Для n, если k+2 ≤ n, то (n−(k+1))^(k+2) < n↓(k+2).
LaTeX
$$(n - (k + 1))^{(k + 2)} < n.descFactorial (k + 2)$$
Lean4
theorem pow_sub_lt_descFactorial' {n : ℕ} : ∀ {k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
| 0, h => by
rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]
exact Nat.mul_lt_mul_of_pos_left (by cutsat) (Nat.sub_pos_of_lt h)
| k + 1, h => by
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
rw [succ_sub_succ]
exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)
