chore(algebra/order*): move `abs`/`min`/`max`, review (#4581)
* make `algebra.ordered_group` import `algebra.order_functions`, not vice versa;
* move some proofs from `algebra.ordered_functions` to `algebra.ordered_group` and `algebra.ordered_ring`;
* deduplicate API;
* golf some proofs.
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
