int_add_neg_l@{} (x : Int) : - x + x = 0. Proof. induction x as [|x IHx|x IHx]. - reflexivity. - by rewrite int_neg_succ, int_add_pred_l, int_add_succ_r, IHx. - by rewrite int_neg_pred, int_add_succ_l, int_add_pred_r, IHx. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.