proposition: Lemma ℤ_ℕ_equiv : forall k π, (0 <= k)%Z -> (π ∈ ‖ℕ (Z.to_nat k)‖ <-> π ∈ ‖ℤ k‖).
proof: Proof. intros k π Hk. unfold ℕ,ℤ. now split; Ksolve; rewrite Z2Nat.id in *; try ok. Qed.
imports: ZArith ClassicalRealizability.Kbase