int_neg@{} (x : Int) : Int := match x with | posS x => negS x | zero => zero | negS x => posS x end.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.