chore(order/basic): rename monotonicity concepts (#9383)
This:
* Renames various mono lemmas either to enable dot notation (in some cases for types that don't exist yet) or to reflect they indicate monotonicity within a particular domain.
* Renames `strict_mono.top_preimage_top'` to `strict_mono.maximal_preimage_top'`
* Sorts some imports
* Replaces some `rcases` with `obtain`
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
