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