proposition: Lemma as_Moebius_Q_product: forall mu mu' (q:Q), denom_nonvanishing_M mu' q -> -1 <= as_Moebius_Q mu' q -> as_Moebius_Q mu' q <= 1 -> Is_refining_M mu -> as_Moebius_Q (product mu mu') q = as_Moebius_Q mu (as_Moebius_Q mu' q).
proof: Proof. intros mu mu' q H_denom. qZ_numerals. intros H_l H_r H_refining. apply Q_to_R_Qeq. realify_Q. intros H_l H_r. assert (H1: denom_nonvanishing_M mu (as_Moebius mu' q)); [apply Is_refining_M_denom_nonvanishing_M; trivial; revert H_l H_r; rewrite Q_to_R_as_Moebius; auto|]. assert (H2: denom_nonvanishing_M (product mu mu') q); [apply denom_nonvanishing_M_product; trivial;revert H_l H_r; rewrite Q_to_R_as_Moebius; auto|]. revert H_l H_r; repeat rewrite Q_to_R_as_Moebius; trivial. intros H_l H_r. apply as_Moebius_product; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M