proposition: Lemma real_value_R:forall alpha, real_value (Cons RR alpha) = (((real_value alpha) +1 )/(-(real_value alpha)+ 3))%R.
proof: Proof. intros alpha; unfold real_value; destruct (R_complete (fun n : nat => lb (Cons RR alpha) n) (lb_Cauchy (Cons RR alpha))) as [x H_x]; destruct (R_complete (fun n : nat => lb alpha n) (lb_Cauchy alpha)) as [y Hy]; simpl; apply SeqProp.UL_sequence with (fun n : nat => lb (Cons RR alpha) n); trivial; apply CV_shift_S'; apply CV_extensionality with (fun n=>(((lb alpha n) + 1) / (-(lb alpha n) + 3))%R). intro n; rewrite lb_S_n; set (l':=lb alpha n); assert (H_min_l'_one_nonneg: Zero <= -l'+1); [stepr (1-l'); try ring; apply Qle_Qminus_Zero; subst l'; apply lb_is_in_base_interval_up|]; assert (H_min_l'_three_pos: Zero < -l'+3); [ apply Qle_lt_trans with ((-l')+1); auto; apply Qlt_Zero_Qminus; stepr 2; auto; qnat_S 2; qnat_S 1; qnat_one; ring|]; auto. unfold hd, tl; fold l'; rewrite as_Moebius_Q_R; trivial; unfold tl; rewrite Q_to_Rdiv; auto; do 2 rewrite Q_to_Rplus; rewrite Q_to_Ropp; do 2 rewrite Z_to_Q_to_R_IZR; simpl; replace (2+1)%R with 3%R; trivial; ring. apply (Rsqrt_def.continuity_seq (fun y=>((y + 1) / (-y + 3))%R) (lb alpha) y); trivial; unfold Ranalysis1.continuity_pt; unfold Rderiv.continue_in; unfold Rdiv; apply (Rlimit.limit_mul (fun y=>(y+1)%R) (fun y=>(Rinv (-y+3)))). apply (Rlimit.limit_plus (fun y=>y) (fun y=>1%R)). apply Rlimit.lim_x. apply (Rlimit.limit_free (fun y=>1%R)); exact y. apply (Rlimit.limit_inv (fun y=>(-y+3)%R)). apply (Rlimit.limit_plus (fun y=>(Ropp y)) (fun y=>3%R)). apply (Rlimit.limit_Ropp (fun y=>y)); apply Rlimit.lim_x. apply (Rlimit.limit_free (fun y=>3%R)); exact y. apply Rlt_not_eq'; unfold Un_cv in Hy; destruct (Hy 2%R) as [N H_N]; try red; auto; assert (H_N_le:N>=N); auto; destruct (Rbasic_fun.Rabs_def2 _ _ (H_N N H_N_le)) as [H1 H2]; generalize (Q_to_Rle _ _ (lb_is_in_base_interval_up N alpha)); rewrite Q_to_R_Qone. apply very_sepcific_1; trivial. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs