proposition: Lemma negate_mult x : -x = - 1 * x.
proof: Proof. apply (left_cancellation (+) x). path_via 0. - apply right_inverse. - path_via (1 * x + (- 1) * x). + apply symmetry. rewrite <-distribute_r. rewrite right_inverse. apply left_absorb. + apply ap011;try reflexivity. apply left_identity. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra