English
On the quadratic integers Z√d (with d non-square), there is a natural preorder defined by the usual order. This preorder is reflexive and transitive, and the strict order is described by the usual lt-iff-le-not-ge relation derived from the base order.
Русский
На квадратичных целых числах Z√d (при ненскорке d) существует естественный предпорядок, задаваемый обычным неравенством. Этот предпорядок рефлексивен и транзитивен, а строгий порядок описывается отношением lt через le и not ge, как в обычном естественном порядке.
LaTeX
$$$$\\text{There exists a preorder } \\le \\text{ on } \\mathbb{Z}\\sqrt{d} \\text{ with reflexivity, transitivity, and } \\text{lt\_iff\_le\_not\_ge} \\; \\le \\text{ the usual order on } \\mathbb{Z}\\sqrt{d}. $$$$
Lean4
instance preorder : Preorder (ℤ√d) where
le := (· ≤ ·)
le_refl a := show Nonneg (a - a) by simp only [sub_self]; trivial
le_trans a b c hab hbc := by simpa [sub_add_sub_cancel'] using hab.add hbc
lt := (· < ·)
lt_iff_le_not_ge _ _ := (and_iff_right_of_imp (Zsqrtd.le_total _ _).resolve_left).symm
