∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : M → α),
  (∀ (a b : M), ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b → f a ≤ f b) →
    ∀ (a b : M), ArchimedeanClass.mk a = ArchimedeanClass.mk b → f a = f b