proposition: Lemma minℕ_realizer : forall e, ℤmin↓e ⊩ ∀₂n,m∈ℕ×ℕ, ℕ (min n m).
proof: Proof. intro e. start. unfold ℕ in Hπ. destruct (Z_le_dec _ _). Kevals. apply mℤ_storage. rewrite Nat2Z.inj_min in *. rewrite Z.min_l in *. now find. assumption. Kevals. apply mℤ_storage. rewrite Nat2Z.inj_min in *. rewrite Z.min_r in *. now find. omega. Qed.
imports: ZArith ClassicalRealizability.Kbase