x y : - (x * y) = -y * -x. 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.
Require Import