proposition: Lemma ℤmax_realizer : forall e, ℤmax↓e ⊩ ∀₂n,m∈ℤ×ℤ, ℤ (Z.max n m).
proof: Proof. intro e. start. destruct (Z_le_dec n m). Kevals. apply mℤ_storage. rewrite Z.max_r in *. find. assumption. Kevals. apply mℤ_storage. rewrite Z.max_l in *. find. omega. Qed.
imports: ZArith ClassicalRealizability.Kbase