proposition: Lemma Q_to_R_Qlt:forall x y : Q, Rlt (Q_to_R x) (Q_to_R y) -> Qlt x y.
proof: Proof. intros x y H_Rlt; destruct (Q_le_lt_dec y x) as [Hxy|Hxy]; trivial; apply False_ind; generalize (Q_to_Rle _ _ Hxy); apply RIneq.Rlt_not_le; assumption. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)