proposition: Lemma Is_refining_M_step_productive_h: forall n mu alpha, Is_refining_M mu -> step_productive_h n mu alpha.
proof: Proof. induction n; intros mu alpha H_refining. constructor; apply Is_refining_M_emits_h; trivial. apply (step_productive_h_S n _ _ (Is_refining_M_emits_h _ alpha H_refining)). apply IHn. apply (Is_refining_M_modulus_h _ alpha H_refining). Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M