proposition: Lemma Z_interpolation: forall x y:R, y > x+1 -> exists n:Z, x < IZR n < y.
proof: Proof. intros. exists (up x). split; auto with real. eapply Rle_lt_trans; [ | eassumption ]. destruct (archimed x). lra. Qed.
imports: Reals Qreals Lra