proposition: Lemma denom_nonvanishing_M_product_inv_M: forall mu r, denom_nonvanishing_M mu r -> ((-1/3) <= as_Moebius mu r <= 1/3)%R -> denom_nonvanishing_M (product inv_MM mu) r.
proof: Proof. intros ((a,b),(c,d)) r; unfold product, as_Moebius, denom_nonvanishing_M, inv_MM, fst, snd; intros H_denom [Hr1 Hr2]; realify_Q; auto; simpl; stepl (1/3*(c*r+d)); auto; field; repeat apply Rmult_resp_nonzero; auto; stepl 3; auto; ring. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M