proposition: Lemma Is_refining_T_productive_q: forall xi alpha beta, Is_refining_T xi -> productive_q xi alpha beta.
proof: Proof. intros xi alpha beta H_refining. constructor; intros n; apply Is_refining_T_step_productive_q; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M