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