proposition: Theorem Rlt_trans_realizer : forall e, Rlt_trans↓e ⊩ ∀ x y z, Cauchy y → (x << y → y << z → x << z)%Re.
proof: Proof. intro e. Kmove. exists Z; split; [| ok]. Kmove. exists Z; split; [| ok]. startn 14. eapply prop_guard. now Ksolve; apply Qclt_le_weak. intro Hle. Kmove. exists ε₁, (ε + ε0). find. rewrite <- Qcplus_0_l at 1. now apply Qcplus_lt_compat. rewrite Qcabs_le_condition in Hle. clear_realizers. revert Hc2 Hc6 Hle. clear. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions