int_add_0_r@{} (x : Int) : x + 0 = x. Proof. induction x as [|[|x] IHx|[|x] IHx]. - reflexivity. - reflexivity. - change (?z.+1 + 0) with (z + 0).+1. exact (ap _ IHx). - reflexivity. - change (?z.-1 + 0) with (z + 0).-1. exact (ap _ 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.