proposition: Theorem Zfloor_imp : forall n x, (IZR n <= x < IZR (n + 1))%R -> Zfloor x = n.
proof: Proof. intros n x Hnx. apply Zle_antisym. apply Zlt_succ_le. apply lt_IZR. apply Rle_lt_trans with (2 := proj2 Hnx). apply Zfloor_lb. now apply Zfloor_lub. Qed.
imports: Coq(Psatz Reals ZArith) Zaux