Is there a theorem in mathlib proving this nat inequality

Stream: Is there code for X?

[Wenrong Zou]

We have the easy inequality saying that for all natural number $q, n$, $1 < q$ then $n\le q^n$. But I don't find a theorem in mathlib about this. (I think it is useful and I guess I should it has been already place in mathlib somewhere ). Thanks in advance!

import Mathlib

theorem nat_inequality {i q: ℕ} (lt_q : 1 < q) : i ≤ q ^ i := by
  induction i with
  | zero => simp
  | succ k ih =>
    if hk₀ : k = 0 then simp [hk₀]; linarith
    else
    rw [pow_add]
    calc
      _ ≤ q^k * 2 := by omega
      _ ≤ _ := (pow_one q).symm ▸ (Nat.mul_le_mul_left (q ^ k) lt_q)

[Ruben Van de Velde]

import Mathlib

theorem nat_inequality {i q: ℕ} (lt_q : 1 < q) : i ≤ q ^ i := by
  exact (Nat.lt_pow_self lt_q).le

[Wenrong Zou]

Thanks!

[Ruben Van de Velde]

I used https://loogle.lean-lang.org/?q=%3Fi+%E2%89%A4+_+^+%3Fi , didn't find anything relevant, wondered if the stronger result was true, and immediately found it with https://loogle.lean-lang.org/?q=%3Fi+%3C+_+%5E+%3Fi

[Wenrong Zou]

Thank you for showing me how to use Loogle to search this!