proposition: Lemma Is_refining_M_product_hd:forall mu alpha, Is_refining_M mu -> Is_refining_M (product mu (map_digits (hd alpha))).
proof: Proof. intros mu [[ | | ] alpha] H_mu; unfold hd; apply Is_refining_M_product; trivial; [apply Is_refining_M_L|apply Is_refining_M_R|apply Is_refining_M_M]. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M