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