proposition: Lemma base_Int_part : forall r:R, IZR (Int_part r) <= r /\ IZR (Int_part r) - r > -1.
proof: Proof. intro; unfold Int_part; elim (archimed r); intros. split; rewrite <- (Z_R_minus (up r) 1); simpl. - apply Rminus_le. replace (IZR (up r) - 1 - r) with (IZR (up r) - r - 1) by ring. now apply Rle_minus. - apply Rminus_gt. replace (IZR (up r) - 1 - r - -1) with (IZR (up r) - r) by ring. now apply Rgt_minus. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac