proposition: Theorem Rle_antisym_realizer : forall e, Rle_antisym↓e ⊩ ∀ x y, (x <= y → y <= x → x ≡ y)%Re.
proof: Proof. intro e. startn 9. eapply prop_guard. Kmove. exists ε₁. find. intro Hle₁. Kmove. exists ε₂, ε₁. find. apply (prop_subst_stack Hπ). clear_realizers. intro Hle₂. rewrite Qcabs_diff_le_condition. revert Hle₁ Hle₂. Qcunfold. lra. Qed.
imports: QArith Psatz ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions