proposition: Lemma negate_sg_op x y : - (x * y) = -y * -x.
proof: Proof. rewrite <- (left_identity (-y * -x)). rewrite <- (left_inverse (unit:=mon_unit) (x * y)). rewrite <- simple_associativity. rewrite <- simple_associativity. rewrite (associativity y). rewrite right_inverse. rewrite (left_identity (-x)). rewrite right_inverse. apply symmetry, right_identity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra