proposition: Lemma maxℕ_realizer : forall e, ℤmax↓e ⊩ ∀₂n,m∈ℕ×ℕ, ℕ (max n m).
proof: Proof. Ksolve. unfold ℕ in *. destruct (Z_le_dec _ _). Kevals. apply mℤ_storage. findn 3. rewrite Nat2Z.inj_max in *; rewrite Z.max_r in *. now apply Hπ. assumption. Kevals. apply mℤ_storage. findn 3. rewrite Nat2Z.inj_max in *. rewrite Z.max_l in *. now apply Hπ. omega. Qed.
imports: ZArith ClassicalRealizability.Kbase