proposition: Theorem Req_Rle_subtype : forall x y, (x ≡ y ⊆ x <= y)%Re.
proof: Proof. unfold Req, Rle. intros x y π Hπ. dec π. 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