proposition: Lemma real_value_M:forall alpha, real_value (Cons MM alpha) = ((real_value alpha)/3)%R.
proof: Proof. intros alpha; unfold real_value; destruct (R_complete (fun n : nat => lb (Cons MM alpha) n) (lb_Cauchy (Cons MM 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 MM alpha) n); trivial; apply CV_shift_S'; apply CV_extensionality with (fun n=>((lb alpha n)/3)%R). intro n; rewrite lb_S_n; rewrite as_Moebius_Q_M; unfold tl; rewrite Q_to_Rdiv; auto. 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/3)%R) (lb alpha) y); trivial; unfold Ranalysis1.continuity_pt; unfold Rderiv.continue_in; unfold Rdiv; apply (Rlimit.limit_mul (fun y=>y) (fun y=>(Rinv 3))). apply Rlimit.lim_x. apply (Rlimit.limit_inv (fun y=>(3)%R)); auto. apply (Rlimit.limit_free (fun y=>3%R)); exact y. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs