proposition: Theorem Zfloor_lub : forall n x, (IZR n <= x)%R -> (n <= Zfloor x)%Z.
proof: Proof. intros n x Hnx. apply Zlt_succ_le. apply lt_IZR. apply Rle_lt_trans with (1 := Hnx). unfold Z.succ. rewrite plus_IZR. apply Zfloor_ub. Qed.
imports: Coq(Psatz Reals ZArith) Zaux