Int_ind@{i} (P : Int -> Type@{i}) (H0 : P 0) (HP : forall n : nat, P n -> P (int_succ n)) (HN : forall n : nat, P (- n) -> P (int_pred (-n))) : forall x, P x. Proof. intros[x | | x]. - induction x as [|x IHx]. + apply (HN 0%nat), H0. + apply (HN x.+1%nat), IHx. - exact H0. - induction x as [|x IHx]. * apply (HP 0%nat), H0. * apply (HP x.+1%nat), 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.