proposition: Lemma not_Qlt:forall x y, ~(Qlt y x) -> (Qle x y).
proof: Proof. intros x y. destruct (Q_le_lt_dec x y); trivial. Qed.
imports: QArithSternBrocot(Q_ordered_field_properties) QArithSternBrocot(R_addenda) Coq(Raxioms) Coq(RIneq)