proposition: Lemma as_Moebius_M: forall mu r, denom_nonvanishing_M mu r -> ((-1)<=as_Moebius mu r<=1)%R-> as_Moebius (product MM mu) r= ((as_Moebius mu r)/3)%R.
proof: Proof. intros ((a,b),(c,d)) r H_denom H_r. generalize (denom_nonvanishing_M_product _ _ _ Is_refining_M_M H_r H_denom); generalize H_denom H_r; clear H_denom H_r. unfold product, as_Moebius, denom_nonvanishing_M, map_digits, fst, snd. realify_Q ;auto; simpl. replace (2+1) with 3; [|ring]. intros H_denom Hr H_denom_product. rewrite Rdiv_Rdiv_Rmult_numerator; auto. apply (f_equal2 Rdiv); field; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M