x y : -(x * y) = x * -y. Proof. lhs nrapply negate_mult_r. lhs_V rapply (simple_associativity (f := (.*.)) x y). apply (ap (x *.)). symmetry. apply negate_mult_r. Defined.
Require Import Require Import