proposition: Lemma Qlt_dr_lt: forall x y:dyadic_rational, (dr2Q x < dr2Q y)%Q -> dr_lt x y.
proof: Proof. intros. destruct (dr_total_order x y) as [|[|]]; [ trivial | apply dr2Q_wd in H0 | apply dr2Q_incr in H0 ]; contradict H0; auto with qarith. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals