proposition: Lemma rationals_dense_in_reals: forall x y:R, x<y -> exists q:Q, x < Q2R q < y.
proof: Proof. intros. pose (d := up (/ (y - x))). assert (0 < d)%Z. { apply lt_IZR, Rlt_trans with (/ (y - x)). - apply Rgt_minus in H. auto with real. - apply archimed. } assert (/ (y - x) < IZR d) by apply archimed. destruct d as [|d|]; try discriminate H0. destruct (rational_interpolation x y d) as [n]; trivial. - replace (1 / (y-x)) with (/(y-x)); lra. - now exists (n # d). Qed.
imports: Reals Qreals Lra