proposition: Lemma Incl_M_absorbs_Is_refining_M:forall mu d, Incl_M mu d -> Is_refining_M (product (inv_digit d) mu).
proof: Proof. intros mu [ | | ] H_Incl; unfold inv_digit; [ apply Incl_M_absorbs_Is_refining_M_L | apply Incl_M_absorbs_Is_refining_M_R | apply Incl_M_absorbs_Is_refining_M_M ]; assumption. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M