proposition: Lemma ℕsub_realizer : forall e, ℕsub↓e ⊩ ∀₂n,m∈ℕ×ℕ, ℕ (n-m).
proof: Proof. intro e. start. destruct (Z_le_dec (Z.of_nat n) (Z.of_nat m)). rewrite <- Nat2Z.inj_le in *. rewrite minus_is_0 in *. Kevals. apply mℕ_storage. find. easy. Kevals. apply ℤsub_realizer. unfold ℕ in *. dec π. find. start. apply Ht. find. rewrite <- Nat2Z.inj_sub. reflexivity. omega. Qed.
imports: ZArith ClassicalRealizability.Kbase