∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K},
  ArchimedeanClass.FiniteResidueField.mk x < ArchimedeanClass.FiniteResidueField.mk y ↔
    x < y ∧ ArchimedeanClass.FiniteResidueField.mk x ≠ ArchimedeanClass.FiniteResidueField.mk y