proposition: Theorem Ropp_involutive_realizer : forall e, λ"_" λ"_" callcc↓e ⊩ ∀x, -(- x) ≤ x.
proof: Proof. unfold Rle, Ropp. intro. do 2 Ksolve. apply Qclt_le_weak. eok. apply Qcle_lt_or_eq in Hc0. destruct Hc0. apply Qcopp_lt_compat in H. eapply (↓x). eassumption. now rewrite Qcopp_involutive. rewrite H. now rewrite Qcopp_involutive. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals