proposition: Lemma Rminus_Int_part2 : forall r1 r2:R, frac_part r1 < frac_part r2 -> Int_part (r1 - r2) = (Int_part r1 - Int_part r2 - 1)%Z.
proof: Proof. intros r1 r2 H; symmetry. apply (Int_part_frac_part_spec _ _ (frac_part r1 - frac_part r2 + 1)). - split. + apply (Rplus_le_reg_r (- 1)). rewrite !Rplus_assoc, Rplus_opp_r, Rplus_0_r. apply Rplus_le_compat. * now apply Rge_le, base_fp. * apply Ropp_le_contravar; left; apply base_fp. + rewrite <-(Rplus_0_l 1) at 2. now apply Rplus_lt_compat_r, Rlt_minus_0. - rewrite (Rplus_Int_part_frac_part r1) at 1. rewrite (Rplus_Int_part_frac_part r2) at 1. rewrite !minus_IZR, Rplus_minus_swap, Rminus_def at 1. rewrite Ropp_plus_distr, !Rplus_assoc, (Rplus_comm _ (frac_part r1)). unfold Rminus. rewrite (Rplus_assoc _ (- 1)), (Rplus_comm (- 1)). now rewrite !Rplus_assoc, Rplus_opp_r, Rplus_0_r. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac