proposition: Lemma Q_to_R_Qle:forall x y : Q, Rle (Q_to_R x) (Q_to_R y) -> Qle x y.
proof: Proof. intros x y H_Rle; destruct (Q_le_lt_dec x y) as [Hxy|Hxy]; trivial; apply False_ind; generalize (Q_to_Rlt _ _ Hxy); apply RIneq.Rle_not_lt; assumption. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)