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