proposition: Theorem Zfloor_ub : forall x : R, (x < IZR (Zfloor x) + 1)%R.
proof: Proof. intros x. unfold Zfloor. rewrite minus_IZR. unfold Rminus. rewrite Rplus_assoc. rewrite Rplus_opp_l, Rplus_0_r. exact (proj1 (archimed x)). Qed.
imports: Coq(Psatz Reals ZArith) Zaux