proposition: Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y.
proof: Proof. intros. now apply Qle_Rle, Qle_bool_imp_le. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant