(n : Int) : Int := match n with | posS (S n) => posS n | 1 => 0 | 0 => -1 | negS n => negS (S n) end.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.