∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk (a * b) ↔ MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b