proposition: Lemma base_fp : forall r:R, frac_part r >= 0 /\ frac_part r < 1.
proof: Proof. intro; unfold frac_part; unfold Int_part; split. - cut (r - IZR (up r) >= -1). + rewrite <- Z_R_minus; simpl; intro; unfold Rminus; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; fold (r - IZR (up r)); fold (r - IZR (up r) - -1); apply Rge_minus; auto with zarith real. + rewrite <- Ropp_minus_distr; apply Ropp_le_ge_contravar; elim (for_base_fp r); auto with zarith real. - cut (r - IZR (up r) < 0). + rewrite <- Z_R_minus; simpl; intro; unfold Rminus; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; fold (r - IZR (up r)); rewrite Ropp_involutive; elim (Rplus_ne 1); intros a b; pattern 1 at 2; rewrite <- a; clear a b; rewrite (Rplus_comm (r - IZR (up r)) 1); apply Rplus_lt_compat_l; auto with zarith real. + elim (for_base_fp r); intros; rewrite <- Ropp_0; rewrite <- Ropp_minus_distr; apply Ropp_gt_lt_contravar; auto with zarith real. Qed.
imports: Rdefinitions Raxioms RIneq ZArith Ztac