∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  (∀ (a : M), a ≠ 0 → ∀ (b : M), b ≠ 0 → ArchimedeanClass.mk a = ArchimedeanClass.mk b) → Archimedean M