int_add_assoc@{} (x y z : Int) : x + (y + z) = x + y + z. Proof. induction x as [|x IHx|x IHx] in y, z |- *. - reflexivity. - by rewrite !int_add_succ_l, IHx. - by rewrite !int_add_pred_l, 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.