int_add_neg_r@{} (x : Int) : x - x = 0. Proof. unfold "-"; by rewrite int_add_comm, int_add_neg_l. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.