proposition: Lemma negate_mult_negate x y : -x * -y = x * y.
proof: Proof. rewrite <-negate_mult_distr_l, <-negate_mult_distr_r. apply involutive. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra