proposition: Lemma Is_refining_M_emits_h: forall mu alpha, Is_refining_M mu -> emits_h mu alpha.
proof: Proof. intros mu alpha H_r. set (smodu:=semantic_modulus_h mu alpha H_r). set (n:=projS1 smodu). assert (Hn:n=(projT1 smodu)); trivial. apply Is_refining_M_emits_h_pointwise with n H_r; trivial. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M