proposition: Theorem Is_refining_M_productive_h: forall mu alpha, Is_refining_M mu -> productive_h mu alpha.
proof: Proof. intros mu alpha H_refining. constructor; intros n; apply Is_refining_M_step_productive_h; trivial. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M