proposition: Lemma nats_Z_ind : forall P : Z -> Prop, (forall n : nat, P n) -> (forall n : nat, P (- n)%Z) -> forall z : Z, P z.
proof: Proof. intros P H H0 z. elim (Z_exh z); intro H1. elim H1; intros x H2. rewrite H2. apply H. elim H1; intros x H2. rewrite H2. apply H0. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid