proposition: Lemma comp_realizer : forall n m A e, comp↓e ⊩ {Z.of_nat n} → {Z.of_nat m} → (n < m ↦ A) → (n = m ↦ A) → (n > m ↦ A) → A.
proof: Proof. intros n m A e. startn 9. apply ℤle_realizer2. findn 6. exists A. find. startn 4. apply ℤeq_realizer2. find. now rewrite Nat2Z.inj_iff. Ksolve. omega. Ksolve. omega. Qed.
imports: ZArith Classical ClassicalRealizability.Kbase ClassicalRealizability.Integers