int_mul_comm@{} (x y : Int) : x * y = y * x. Proof. induction y as [|y IHy|y IHy] in x |- *. - apply int_mul_0_r. - rewrite int_mul_succ_l. rewrite int_mul_succ_r. by rewrite IHy. - rewrite int_mul_pred_l. rewrite int_mul_pred_r. by rewrite IHy. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.