proposition: Lemma Rminus_fp2 : forall r1 r2:R, frac_part r1 < frac_part r2 -> frac_part (r1 - r2) = frac_part r1 - frac_part r2 + 1.
proof: Proof. intros r1 r2 H%Rminus_Int_part2; unfold frac_part. rewrite H, !minus_IZR; unfold Rminus; rewrite !Ropp_plus_distr, !Ropp_involutive. rewrite (Rplus_assoc r1), <-!(Rplus_assoc (- r2)), (Rplus_comm (- r2)). now rewrite !Rplus_assoc. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac