proposition: Lemma ℤlt_realizer : forall e, ℤlt↓e ⊩ ∀₂n,m∈ℤ×ℤ, ∀ A B, ((n < m)%Z ↦ A) → ((~n < m)%Z ↦ B) → ((n < m)%Z ↦ A) ∩ ((~n < m)%Z ↦ B).
proof: Proof. intro. startn 6. apply ℤadd_realizer. find. start. apply ℤle_realizer. find. find. rewrite mapsto_equiv in Ht |- *. intro. apply Ht. omega. rewrite mapsto_equiv in Ht0 |- *. intro. apply Ht0. omega. destruct Hπ as [[]|[]]; [left | right]; split; assumption || omega. Qed.
imports: ZArith ClassicalRealizability.Kbase