proposition: Lemma pred_succ_Z_ind : forall P : Z -> Prop, P 0%Z -> (forall n : Z, P n -> P (n + 1)%Z) -> (forall n : Z, P n -> P (n - 1)%Z) -> forall z : Z, P z.
proof: Proof. intros P H H0 H1 z. apply nats_Z_ind. intro n. elim n. exact H. intros n0 H2. replace (S n0:Z) with (n0 + 1)%Z. apply H0. assumption. rewrite Znat.inj_S. reflexivity. intro n. elim n. exact H. intros n0 H2. replace (- S n0)%Z with (- n0 - 1)%Z. apply H1. assumption. rewrite Znat.inj_S. unfold Z.succ in |- *. rewrite Zopp_plus_distr. reflexivity. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid