feat(algebra/ordered_group): add `order_iso.inv` (#8492)
* add `order_iso.inv` and `order_iso.neg`;
* use it to golf a few proofs;
* use `alias` to generate some `imp` lemmas from `iff` lemmas;
* generalize some lemmas about `order_iso` from `preorder` to `has_le`.
