int_succ_pred@{} (x : Int) : x.+1.-1 = x. Proof. by destruct x as [[] | | ]. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.