(n m : nat) : (n * m)%int = (n * m)%nat :> Int. Proof. induction n as [|n IHn]. - reflexivity. - rewrite <- int_nat_succ. rewrite int_mul_succ_l. rewrite nat_mul_succ_l. rhs_V nrapply int_nat_add. exact (ap _ IHn). Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.