proposition: Lemma semantic_modulus_h: forall mu alpha, Is_refining_M mu -> {n:nat & { d | Incl_M (product_init mu alpha n) d /\ (forall m d', (m<n)%nat ->~Incl_M (product_init mu alpha m) d') } }.
proof: Proof. intros mu alpha H_r. apply LNP_sigS_nat_Digit. intros n d; apply Incl_M_dec_D. apply thesis_5_6_10; assumption. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M