proposition: Lemma Int_part_frac_part_spec : forall r z f, 0 <= f < 1 -> r = (IZR z) + f -> z = Int_part r /\ f = frac_part r.
proof: Proof. intros r z f [Hlef Hltf] E%(Rminus_eq_compat_r f); rewrite Rplus_minus_r in E. assert (IP : z = Int_part r). { apply Int_part_spec; split. - now rewrite <-E; apply Rplus_lt_compat_l, Ropp_lt_contravar. - rewrite <-E; apply (Rplus_le_reg_r f). rewrite <-Rplus_minus_swap, Rplus_minus_r, <-(Rplus_0_r r) at 1. now apply Rplus_le_compat_l. } split; try easy. unfold frac_part. now rewrite <-IP, <-E, Rminus_def, Ropp_minus_distr, Rplus_minus. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac