proposition: Lemma real_value_base_interval:forall alpha, (-1 <= real_value alpha <= 1)%R.
proof: Proof. intros alpha; unfold real_value. destruct (R_complete (fun n : nat => lb alpha n) (lb_Cauchy alpha)) as [y Hy]; simpl; generalize RiemannInt.Rle_cv_lim; intro H_sandwich; split. apply (H_sandwich (fun (n:nat)=>(-1)%R) (fun n : nat => lb alpha n) (-1)%R y); trivial. intros n; rewrite <- Q_to_R_Qneg_One; apply Q_to_Rle; apply lb_is_in_base_interval_low. apply CV_const. apply (H_sandwich (fun n : nat => lb alpha n) (fun (n:nat)=>(1)%R) y (1)%R); trivial. intros n; rewrite <- Q_to_R_Qone; apply Q_to_Rle; apply lb_is_in_base_interval_up. apply CV_const. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs