proposition: Lemma preserves_negate x : f (-x) = -f x.
proof: Proof. apply (left_cancellation (&) (f x)); rewrite <- preserves_sg_op; group_simplify; apply preserves_mon_unit. Qed.
imports: Coq.Classes.Morphisms MathClasses.interfaces.abstract_algebra