proposition: Lemma as_Moebius_product : forall mu mu' r, denom_nonvanishing_M mu' r -> ((-1)<=as_Moebius mu' r<=1)%R -> Is_refining_M mu -> as_Moebius (product mu mu') r = as_Moebius mu (as_Moebius mu' r).
proof: Proof. intros ((a,b),(c,d)) ((a',b'),(c',d')) r H_denom H_mu'_r H_refining. generalize (denom_nonvanishing_M_product _ _ _ H_refining H_mu'_r H_denom). generalize H_denom; clear H_denom. unfold as_Moebius, denom_nonvanishing_M, product, fst, snd. realify_Q. intros H_denom H_denom_prod. repeat rewrite Rdiv_Rmult_numerator; trivial. repeat rewrite Rdiv_Rplus_Rmult; trivial. rewrite Rdiv_Rdiv_simplify; trivial. apply (f_equal2 Rdiv); ring. stepl ((c * a' + d * c') * r + (c * b' + d * d')); trivial; ring. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M