feat(order/basic): More order instances for `subtype` (#13134)
Add the `has_le`, `has_lt`, `decidable_le`, `decidable_lt`, `bounded_order` instances.
Incorporating the `decidable_le` and `decidable_lt` instances into the `linear_order` one breaks some defeqs with `ite`/`dite`.
