proposition: Lemma dr2Q_incr: forall x y:dyadic_rational, dr_lt x y -> dr2Q x < dr2Q y.
proof: Proof. induction 1. - unfold dr2Q, Qlt. cbn. apply Zmult_lt_compat_r. + easy. + now apply Znat.inj_lt. - now rewrite <- (dr2Q_wd _ _ H0), <- (dr2Q_wd _ _ H1). Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals