proposition: Lemma Int_part_spec : forall r z, r - 1 < IZR z <= r -> z = Int_part r.
proof: Proof. unfold Int_part; intros r z [Hle Hlt]; apply Z.add_move_r, tech_up. - rewrite <-(Rplus_0_r r), <-(Rplus_opp_l 1), <-Rplus_assoc, plus_IZR. now apply Rplus_lt_compat_r. - now rewrite plus_IZR; apply Rplus_le_compat_r. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac