proposition: Lemma Rminus_Int_part1 : forall r1 r2:R, frac_part r1 >= frac_part r2 -> Int_part (r1 - r2) = (Int_part r1 - Int_part r2)%Z.
proof: Proof. intros r1 r2 H; symmetry. apply (Int_part_frac_part_spec _ _ (frac_part r1 - frac_part r2)). - split. + apply (Rplus_le_reg_r (frac_part r2)). rewrite Rplus_0_l, <-Rplus_minus_swap, Rplus_minus_r. now apply Rge_le. + rewrite <-(Rminus_0_r 1); apply Rplus_lt_le_compat. * now apply base_fp. * now apply Ropp_le_contravar, Rge_le, base_fp. - 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)). now unfold Rminus; rewrite !Rplus_assoc. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac