proposition: Theorem Zeven_ex : forall x, exists p, x = (2 * p + if Z.even x then 0 else 1)%Z.
proof: Proof. intros [|[n|n|]|[n|n|]]. now exists Z0. now exists (Zpos n). now exists (Zpos n). now exists Z0. exists (Zneg n - 1)%Z. change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z. ring. now exists (Zneg n). now exists (-1)%Z. Qed.
imports: Coq(ZArith Lia Zquot)