proposition: Theorem constructive_indefinite_description_Z : ex P -> sig P.
proof: Proof. intros H. case (P_decidable 0). intro. econstructor. eauto. intro nP0. pose (fun n => P (Z_of_nat n) \/ P (- Z_of_nat n)) as P'. assert (ex P'). destruct H as [z]. exists (Z.abs_nat z). destruct z; [contradiction | left | right]; simpl; rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P; assumption. destruct (constructive_indefinite_description_nat P'). intro n. unfold P'. destruct P_decidable with (Z_of_nat n); intuition. destruct P_decidable with (- Z_of_nat n); intuition. assumption. destruct P_decidable with (Z_of_nat x). econstructor; apply p1. destruct P_decidable with (- Z_of_nat x). econstructor; apply p1. subst P'; simpl in *. assert False by tauto. contradiction. Defined.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory ZArith Znumtheory ConstructiveEpsilon