proposition: Lemma rational_interpolation: forall (x y:R) (n:positive), x<y -> IZR (' n) > 1/(y-x) -> exists m:Z, x < Q2R (m # n) < y.
proof: Proof. intros. assert (0 < / IZR (' n)) by auto with real. destruct (Z_interpolation (IZR (' n) * x) (IZR (' n) * y)) as [m]. - apply Rgt_minus in H. assert (IZR (' n) * (y - x) > 1). { replace 1 with ((1 / (y-x)) * (y-x)) by (field; auto with real). now apply Rmult_gt_compat_r. } apply Rgt_minus in H2. apply Rminus_gt. match goal with H2: ?a > 0 |- ?b > 0 => replace b with a end; lra. - exists m. unfold Q2R. simpl. replace x with ((IZR (' n) * x) / IZR (' n)) by (field; auto with real). replace y with ((IZR (' n) * y) / IZR (' n)) by (field; auto with real). destruct H2. split; now apply Rmult_lt_compat_r. Qed.
imports: Reals Qreals Lra