Commit 2021-07-27 08:42 23e7c841

fix(algebra/ordered_group): add missing to_additive, fix simps (#8429)

• Add order_iso.add_left and order_iso.add_right.
• Use to_equiv := instead of .. to ensure rfl : (order_iso.mul_right a).to_equiv = equiv.mul_right a.
• Simplify unapplied (order_iso.mul_left a).symm etc.