English
There is a Preorder structure on MulArchimedeanOrder M induced by the definitions of ≤ and <; in particular, ≤ is reflexive and transitive, and lt corresponds to the standard lt_iff_le_not_ge formulation.
Русский
На MulArchimedeanOrder M задана структура предупорядочения: ≤ рефлексивно и транзитивно, а < эквивалентно lt_iff_le_not_ge.
LaTeX
$$$\text{Preorder}(\text{MulArchimedeanOrder } M) \ \,\text{with } a \le b \text{ as above and } a < b \text{ as above.}$$$
Lean4
@[to_additive]
instance : Preorder (MulArchimedeanOrder M) where
le_refl a := ⟨1, by simp⟩
le_trans a b
c := by
intro ⟨m, hm⟩ ⟨n, hn⟩
use m * n
rw [pow_mul]
exact hn.trans (pow_le_pow_left' hm n)
lt_iff_le_not_ge a
b := by
rw [lt_def, le_def, le_def]
suffices (∀ (n : ℕ), |b.val|ₘ ^ n < |a.val|ₘ) → ∃ n, |b.val|ₘ ≤ |a.val|ₘ ^ n by simpa using this
intro h
obtain h := (h 1).le
exact ⟨1, by simpa using h⟩
