proposition: Lemma preserves_negate x : f (-x) = -f x.
proof: Proof. apply (left_cancellation (.*.) (f x)). rewrite <-preserves_sg_op. rewrite 2!right_inverse. apply preserves_mon_unit. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra