English
If a^2 ≤ b a, then for all n ≠ 0, a^n ≤ b^{n-1} a.
Русский
Если a^2 ≤ b a, то для всех n ≠ 0 верно a^n ≤ b^{n-1} a.
LaTeX
$$$ a^2 \le b a \Rightarrow (\forall n \neq 0,\ a^n \le b^{n-1} a) $$$
Lean4
/-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations. -/
@[to_additive /-- This lemma is useful in non-cancellative monoids, like sets under pointwise operations. -/
]
theorem pow_le_pow_mul_of_sq_le_mul [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b * a) :
∀ {n}, n ≠ 0 → a ^ n ≤ b ^ (n - 1) * a
| 1, _ => by simp
| n + 2, _ => by
calc
a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
_ ≤ b ^ n * a * a := (mul_le_mul_right' (pow_le_pow_mul_of_sq_le_mul hab (by cutsat)) _)
_ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
_ ≤ b ^ n * (b * a) := (mul_le_mul_left' hab _)
_ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]
