{α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : Add α] →
          [inst_3 : Add β] →
            (toAddEquiv : α ≃+ β) → (∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b) → α ≃+o β