proposition: Theorem Ztrunc_lub : forall n x, (IZR n <= Rabs x)%R -> (n <= Z.abs (Ztrunc x))%Z.
proof: Proof. intros n x H. rewrite <- Ztrunc_abs. rewrite Ztrunc_floor. 2: apply Rabs_pos. now apply Zfloor_lub. Qed.
imports: Coq(Psatz Reals ZArith) Zaux