{α : Type u_3} →
  [toAddCommMonoid : AddCommMonoid α] →
    [toLinearOrder : LinearOrder α] →
      [toIsOrderedAddMonoid : IsOrderedAddMonoid α] →
        [toOrderTop : OrderTop α] →
          [toNeg : Neg α] →
            [toSub : Sub α] →
              autoParam (∀ (a b : α), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam →
                (zsmul : ℤ → α → α) →
                  autoParam (∀ (a : α), zsmul 0 a = 0) SubNegMonoid.zsmul_zero'._autoParam →
                    autoParam (∀ (n : ℕ) (a : α), zsmul (↑n.succ) a = zsmul (↑n) a + a)
                        SubNegMonoid.zsmul_succ'._autoParam →
                      autoParam (∀ (n : ℕ) (a : α), zsmul (Int.negSucc n) a = -zsmul (↑n.succ) a)
                          SubNegMonoid.zsmul_neg'._autoParam →
                        [toNontrivial : Nontrivial α] →
                          (∀ (x : α), ⊤ + x = ⊤) →
                            -⊤ = ⊤ → (∀ ⦃x : α⦄, x ≠ ⊤ → x + -x = 0) → LinearOrderedAddCommGroupWithTop α