proposition: Lemma Is_refining_M_product: forall mu mu', Is_refining_M mu -> Is_refining_M mu' -> Is_refining_M (product mu mu').
proof: Proof. intros ((a,b),(c,d)) ((a',b'),(c',d')) H_mu H_mu'. apply Is_refining_M_property_fold; intros r Ht. apply denom_nonvanishing_M_product; trivial; [ apply Is_refining_M_property | apply Is_refining_M_denom_nonvanishing_M ]; trivial. rewrite as_Moebius_product; trivial; repeat apply Is_refining_M_property; trivial; apply Is_refining_M_denom_nonvanishing_M; trivial. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M