(n : nat) : (n.+1)%int = (n.+1)%nat :> Int. Proof. by induction n. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.