int_add_succ_l@{} (x y : Int) : x.+1 + y = (x + y).+1. Proof. induction x as [|[|x] IHx|[|x] IHx] in y |- *. 1-3: reflexivity. all: symmetry; apply int_pred_succ. Defined.
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe. Require Import Spaces.Nat.Core.