proposition: Lemma LPO_Z : forall P : Z -> Prop, (forall n, P n \/ ~P n) -> {n : Z| P n} + {forall n, ~ P n}.
proof: Proof. intros P H. destruct (LPO (fun n => P (Z.of_nat n))) as [J|J]. intros n; apply H. destruct J as (n, Hn). left; now exists (Z.of_nat n). destruct (LPO (fun n => P (-Z.of_nat n)%Z)) as [K|K]. intros n; apply H. destruct K as (n, Hn). left; now exists (-Z.of_nat n)%Z. right; intros n; case (Zle_or_lt 0 n); intros M. rewrite <- (Z.abs_eq n); trivial. rewrite <- Zabs2Nat.id_abs. apply J. rewrite <- (Z.opp_involutive n). rewrite <- (Z.abs_neq n). rewrite <- Zabs2Nat.id_abs. apply K. lia. Qed.
imports: Coq(Psatz Reals ZArith) Zaux