English
If a is a natural number different from 1, then for every natural b, the product a·b does not exceed a^b.
Русский
Если a ∈ ℕ и a ≠ 1, то для каждого b ∈ ℕ выполняется a·b ≤ a^b.
LaTeX
$$$ \forall a,b \in \mathbb{N},\ a \ne 1 \implies a\cdot b \le a^{b} $$$
Lean4
theorem mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) : a * b ≤ a ^ b := by
induction b generalizing a with
| zero => simp
| succ b hb =>
rw [mul_add_one, pow_succ]
rcases a with (_ | _ | a)
· simp
· simp at ha
· rw [mul_add_one, mul_add_one, add_comm (_ * a), add_assoc _ (_ * a)]
rcases b with (_ | b)
· simp [add_comm]
refine add_le_add (hb (by simp)) ?_
rw [pow_succ']
refine (le_add_left ?_ ?_).trans' ?_
exact le_mul_of_one_le_right' (one_le_pow _ _ (by simp))
