proposition: Lemma negate_sg_op_distr_flip `{Group A}: ∀ a b, -(a & b) = -b & -a.
proof: Proof. intros. setoid_replace (-b & -a) with (-(a & b) & (a & b) & (-b & -a)) by group; rewrite <- associativity; setoid_replace (a & b & (-b & -a)) with mon_unit; group. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra