pow_sub_lt_descFactorial — Mathlib

English

If k ≥ 2 and k ≤ n, then (n+1−k)^k < n.descFactorial k.

Русский

Если 2 ≤ k ≤ n, то (n+1−k)^k < n↓k.

LaTeX

$$(2 ≤ k) ∧ (k ≤ n) ⇒ (n + 1 - k)^{k} < n.descFactorial k$$

Lean4

theorem pow_sub_lt_descFactorial {n : ℕ} : ∀ {k : ℕ}, 2 ≤ k → k ≤ n → (n + 1 - k) ^ k < n.descFactorial k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ h => by
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' h

Похожие утверждения