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