proposition: Lemma negate_mult_distr_r x y : -(x * y) = x * -y.
proof: Proof. rewrite negate_mult,(negate_mult y). rewrite simple_associativity,(commutativity (- 1)). apply symmetry,associativity. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra