isinj_int_neg@{} (x y : Int) : - x = - y -> x = y := equiv_inj int_neg.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.