mathlib

1b876c7d - chore(algebra/ordered_group): fix/add `order_dual` instances, add lemmas (#8564)

chore(algebra/ordered_group): fix/add `order_dual` instances, add lemmas (#8564) * add `order_dual.has_inv`, `order_dual.group`, `order_dual.comm_group`; * use new instances in `order_dual.ordered_comm_group` and `order_dual.linear_ordered_comm_group` (earlier we had only additive versions); * add `le_of_forall_neg_add_le`, `le_of_forall_pos_sub_le`, `le_iff_forall_neg_add_le` and their multiplicative versions.