English
On the quotient by zmultiples p, one can define a circular preorder robustly extending the natural order, making the quotient into a circularly ordered set.
Русский
На фактор-группе по zmultiples p можно ввести цилиндрический (кольцевой) порядок, образующий из неё множество с кольцевым порядком.
LaTeX
$$$$ \text{CircularPreorder}((\alpha / \langle p \rangle)) $$$$
Lean4
instance circularPreorder : CircularPreorder (α ⧸ AddSubgroup.zmultiples p)
where
btw_refl x := show _ ≤ _ by simp [sub_self, hp'.out.le]
btw_cyclic_left {x₁ x₂ x₃}
h := by
induction x₁ using QuotientAddGroup.induction_on
induction x₂ using QuotientAddGroup.induction_on
induction x₃ using QuotientAddGroup.induction_on
simp_rw [btw_coe_iff] at h ⊢
apply toIxxMod_cyclic_left _ h
sbtw := _
sbtw_iff_btw_not_btw := Iff.rfl
sbtw_trans_left {x₁ x₂ x₃ x₄} (h₁₂₃ : _ ∧ _)
(h₂₃₄ : _ ∧ _) :=
show _ ∧ _ by
induction x₁ using QuotientAddGroup.induction_on
induction x₂ using QuotientAddGroup.induction_on
induction x₃ using QuotientAddGroup.induction_on
induction x₄ using QuotientAddGroup.induction_on
simp_rw [btw_coe_iff] at h₁₂₃ h₂₃₄ ⊢
apply toIxxMod_trans _ h₁₂₃ h₂₃₄
