chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up (#22109)

* Shorten proofs
* Make the `WithBot` and `WithTop` sections analogous
* Avoid relying on the defeq `(WithTop α)ᵒᵈ = WithBot αᵒᵈ`
* Pull more implicit variables to `variable` statements
* Stick to the convention that `a b : α` and `x y : WithBot α`

This is a follow-up to #21274.

Author: YaelDillies

Mathlib/Algebra/Order/AddGroupWithTop.lean

@@ -7,7 +7,6 @@ import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.CharZero.Defs
-import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 
 /-!