(n m : nat) : (n + m)%int = (n + m)%nat :> Int. Proof. induction n as [|n IHn]. - reflexivity. - rewrite <- 2 int_nat_succ. rewrite int_add_succ_l. 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.