{α : Type u_2} →
  {β : Type u_3} →
    {x : CommGroup α} →
      {x_1 : PartialOrder α} →
        {x_2 : CommGroup β} →
          {x_3 : PartialOrder β} →
            (f : α ≃ β) → (∀ {a b : α}, f a ≤ f b ↔ a ≤ b) → (∀ (a b : α), f (a * b) = f a * f b) → α ≃*o β