proposition: Corollary Rle_refl_realizer : forall e, Rle_refl↓e ⊩ ∀₁x∈Cauchy, (x <= x)%Re.
proof: Proof. Kmove. exists ε₁. find. apply (prop_subst_stack Hπ). rewrite Qcabs_diff_le_condition. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions