English
If x > 1 in a densely ordered monoid with the given structure, then for every n there exists y > 1 with y^n < x.
Русский
Если x > 1 в плотно упорядоченном моноиде с заданной структурой, то для каждого числа n существует y > 1 такое, что y^n < x.
LaTeX
$$$\big( 1 < x \big) \rightarrow \forall n \in \mathbb{N},\ exists\ y>1,\ y^n < x$$$
Lean4
@[to_additive]
theorem exists_pow_lt_of_one_lt (hx : 1 < x) : ∀ n : ℕ, ∃ y : M, 1 < y ∧ y ^ n < x
| 0 => ⟨x, by simpa⟩
| 1 => by simpa using exists_between hx
| n + 2 => by
obtain ⟨y, hy, hyx⟩ := exists_pow_lt_of_one_lt hx (n + 1)
obtain ⟨z, hz, hzy⟩ := exists_pow_two_le_of_one_lt hy
refine ⟨z, hz, hyx.trans_le' ?_⟩
calc
z ^ (n + 2)
_ ≤ z ^ (2 * (n + 1)) := (pow_right_monotone hz.le (by cutsat))
_ = (z ^ 2) ^ (n + 1) := by rw [pow_mul]
_ ≤ y ^ (n + 1) := pow_le_pow_left' hzy (n + 1)
