proposition: Lemma Is_refining_T_emits_q: forall xi alpha beta, Is_refining_T xi -> emits_q xi alpha beta.
proof: Proof. intros xi alpha beta H_r. set (smodu:=semantic_modulus_q xi alpha beta H_r). set (n:=projS1 smodu). assert (Hn:n=(projT1 smodu)); trivial. apply Is_refining_T_emits_q_pointwise with n H_r; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M