proposition: Theorem Zceil_glb : forall n x, (x <= IZR n)%R -> (Zceil x <= n)%Z.
proof: Proof. intros n x Hnx. unfold Zceil. apply Zopp_le_cancel. rewrite Z.opp_involutive. apply Zfloor_lub. rewrite opp_IZR. now apply Ropp_le_contravar. Qed.
imports: Coq(Psatz Reals ZArith) Zaux