proposition: Lemma negate_zero_prod_r x y : x * -y = 0 <-> x * y = 0.
proof: Proof. rewrite (commutativity (f:=(.*.)) x (-y)), (commutativity (f:=(.*.)) x y). apply negate_zero_prod_l. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra