Commit 2021-08-01 21:03 60c378d0

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.