int_mul_pred_r@{} (x y : Int) : x * y.-1 = -x + x * y. Proof. induction x as [|x IHx|x IHx] in y |- *. - reflexivity. - rewrite 2 int_mul_succ_l. rewrite IHx. rewrite !int_add_assoc; f_ap. rewrite <- (int_neg_neg y.-1). rewrite <- int_neg_add. rewrite int_neg_pred. rewrite int_add_succ_l. rewrite int_add_comm. rewrite <- int_add_succ_l. rewrite int_neg_add. by rewrite int_neg_neg. - rewrite int_neg_pred. rewrite int_neg_neg. rewrite 2 int_mul_pred_l. rewrite IHx. rewrite !int_add_assoc; f_ap. rewrite int_neg_pred. rewrite int_neg_neg. rewrite 2 int_add_succ_l; f_ap. by rewrite int_add_comm. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.