chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389)
chore(data/pi/lex): turn `pi.lex.linear_order` into an instance (#14389)

* Use `[is_well_order ι (<)]` instead of `(wf : well_founded ((<) : ι → ι → Prop))`. This way `pi.lex.linear_order` can be an instance.
* Add `pi.lex.order_bot`/`pi.lex.order_top`/`pi.lex.bounded_order`.





leanprover-community/mathlib,leanprover-community/mathlib