proposition: Lemma plus_frac_part1 : forall r1 r2:R, frac_part r1 + frac_part r2 >= 1 -> frac_part (r1 + r2) = frac_part r1 + frac_part r2 - 1.
proof: Proof. intros; unfold frac_part; generalize (plus_Int_part1 r1 r2 H); intro; rewrite H0; rewrite (plus_IZR (Int_part r1 + Int_part r2) 1); rewrite (plus_IZR (Int_part r1) (Int_part r2)); simpl; unfold Rminus at 3 4; rewrite (Rplus_assoc r1 (- IZR (Int_part r1)) (r2 + - IZR (Int_part r2))); rewrite (Rplus_comm r2 (- IZR (Int_part r2))); rewrite <- (Rplus_assoc (- IZR (Int_part r1)) (- IZR (Int_part r2)) r2); rewrite (Rplus_comm (- IZR (Int_part r1) + - IZR (Int_part r2)) r2); rewrite <- (Rplus_assoc r1 r2 (- IZR (Int_part r1) + - IZR (Int_part r2))); rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))); unfold Rminus; rewrite (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); trivial with real. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac