int_mul_neg_r@{} (x y : Int) : x * - y = - (x * y). Proof. rewrite !(int_mul_comm x). apply int_mul_neg_l. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.