proposition: Lemma dr2Q_wd: forall x y:dyadic_rational, dr_eq x y -> dr2Q x == dr2Q y.
proof: Proof. intros. induction H; auto with qarith. { now transitivity (dr2Q y). } unfold Qeq. simpl. change ((' (pos_power2 n)~0)%Z) with ((2 * ' pos_power2 n)%Z). repeat rewrite inj_plus. ring. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals