feat(data/sigma/order): The lexicographical order has a bot/top (#10905)
feat(data/sigma/order): The lexicographical order has a bot/top (#10905)

Also fix localized instances declarations. They weren't using fully qualified names and I had forgotten `sigma.lex.linear_order`.





leanprover-community/mathlib,leanprover-community/mathlib