int_mul_neg_l@{} (x y : Int) : - x * y = - (x * y). Proof. induction x as [|x IHx|x IHx] in y |- *. - reflexivity. - rewrite int_neg_succ. rewrite int_mul_pred_l. rewrite int_mul_succ_l. rewrite int_neg_add. by rewrite IHx. - rewrite int_neg_pred. rewrite int_mul_succ_l. rewrite int_mul_pred_l. rewrite int_neg_add. rewrite IHx. by rewrite int_neg_neg. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.