int_mul_succ_l@{} (x y : Int) : x.+1 * y = y + x * y. Proof. induction x as [|[|x] IHx|[] IHx] in y |- *. - reflexivity. - reflexivity. - reflexivity. - cbn. rewrite int_add_0_r. by rewrite int_add_neg_r. - rewrite int_pred_succ. cbn. rewrite int_add_assoc. rewrite int_add_neg_r. by rewrite int_add_0_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.