proposition: Theorem Rlt_irrefl_realizer : forall e, Rlt_irrefl↓e ⊩ ∀x, Cauchy x → ¬(x << x)%Re.
proof: Proof. Ksolve. start. eapply (prop_realizer2 (A := (Qcle (q₂ - q₁) (ε₁ + ε₂)))). revert Hc0 Hc2. Qcunfold. lra. do 2 Ksolve. now apply Qclt_le_weak. now apply Qclt_le_weak. rewrite Qcabs_minus, Qcabs_le_condition. apply (prop_subst_stack Hπ). now intros [_ ?]. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions