proposition: Theorem Zfloor_lb : forall x : R, (IZR (Zfloor x) <= x)%R.
proof: Proof. intros x. unfold Zfloor. rewrite minus_IZR. simpl. apply Rplus_le_reg_r with (1 - x)%R. ring_simplify. exact (proj2 (archimed x)). Qed.
imports: Coq(Psatz Reals ZArith) Zaux