proposition: Lemma dyadic_rationals_dense_in_reals: forall x y:R, 0 <= x < y -> exists q:dyadic_rational, x < Q2R (dr2Q q) < y.
proof: Proof. intros. assert (forall m:Z, exists n:nat, ((m < ' pos_power2 n)%Z)). { intros. case m; intros; try now exists O. induction p. - destruct IHp as [n]. exists (S n). unfold Z.lt. simpl. rewrite Pos.compare_xI_xO. unfold Z.lt in H0. simpl in H0. now rewrite H0. - destruct IHp as [n]. now exists (S n). - now exists 1%nat. } destruct (H0 (up (1/(y-x)))) as [n]. destruct (rational_interpolation x y (pos_power2 n)) as [m]. - apply H. - eapply Rlt_trans. + apply archimed. + now apply IZR_lt. - destruct m as [|m|]. + unfold Q2R in H2. simpl in H2. replace (0 * _) with 0 in H2 by ring. destruct H, H2. contradict H. auto with real. + exists (m_over_2_to_n (nat_of_P m) n). unfold dr2Q. now rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. + assert (x < 0). { eapply Rlt_trans. - apply H2. - replace 0 with (Q2R 0) by lra. apply Qlt_Rlt. auto with qarith. } lra. Qed.
imports: Coq(Reals Lia Lra ClassicalChoice) RationalsInReals