int_add_succ_r@{} (x y : Int) : x + y.+1 = (x + y).+1. Proof. induction x as [|x IHx|[] IHx] in y |- *. - reflexivity. - by rewrite 2 int_add_succ_l, IHx. - cbn; by rewrite int_succ_pred, int_pred_succ. - change ((- (n.+1%nat)).-1 + y.+1 = ((- (n.+1%nat)).-1 + y).+1). rewrite int_add_pred_l. rewrite IHx. rewrite <- 2 int_add_succ_l. rewrite <- int_add_pred_l. by rewrite int_pred_succ, 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.