refactor(order/bounds): general cleanup (#14127)
Apart from golfing, this PR does the following:
Add the following theorems (which are immediate from the non-self counterparts):
- `monotone_on.mem_upper_bounds_image_self`
- `monotone_on.mem_lower_bounds_image_self`
- `antitone_on.mem_upper_bounds_image_self`
- `antitone_on.mem_lower_bounds_image_self`
Remove the following theorems (as they're just `mem_X_bounds_image` under unnecessarily stronger assumptions):
- `monotone_on.is_lub_image_le`
- `monotone_on.le_is_glb_image`
- `antitone_on.is_lub_image_le`
- `antitone_on.le_is_glb_image`
- `monotone.is_lub_image_le`
- `monotone.le_is_glb_image`
- `antitone.is_lub_image_le`
- `antitone.le_is_glb_image`
Remove a redundant argument `s ⊆ t` from the following (the old theorems follow immediately from the new ones and `monotone_on.mono`):
- `monotone_on.map_is_greatest`
- `monotone_on.map_is_least`
- `antitone_on.map_is_greatest`
- `antitone_on.map_is_least`
