Commit 2021-08-06 17:42 1b876c7d

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.