proposition: Lemma real_value_digits: forall d alpha, real_value (Cons d alpha) = as_Moebius d (real_value alpha).
proof: Proof. intros [ | | ] alpha; unfold as_Moebius, fst, snd, map_digits; [ rewrite real_value_L | rewrite real_value_R | rewrite real_value_M ]; qZ_numerals; realify_Q; auto; field. assert (H_alpha_base:=proj1 (real_value_base_interval alpha)); auto. assert (H_alpha_base:=proj2 (real_value_base_interval alpha)); apply Rlt_not_eq'; Fourier.fourier. Qed.
imports: digits ub rep Rseries Rdefinitions RIneq Rcomplete QArithSternBrocot(R_addenda) Fourier_solvable_ineqs