proposition: Lemma denom_nonvanishing_M_product:forall mu mu' r,Is_refining_M mu ->((-1)<=as_Moebius mu' r<=1)%R-> denom_nonvanishing_M mu' r-> denom_nonvanishing_M (product mu mu') r.
proof: Proof. intros ((a,b),(c,d)) ((a',b'),(c',d')) r. unfold as_Moebius, denom_nonvanishing_M, product, fst, snd. intros H_refining Hr H_denom. repeat rewrite Q_to_Rplus; repeat rewrite Q_to_Rmult. stepl (c*(a'*r+b')+d*(c'*r+d')); [|ring]. apply Rlinear_non_zero_2; auto. apply (Is_refining_M_denom_nonvanishing_M _ _ H_refining Hr). Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M