proposition: Lemma Is_refining_M_modulus_h:forall mu alpha (H_r:Is_refining_M mu), let modu:=modulus_h mu alpha (Is_refining_M_emits_h mu alpha H_r) in let mu' := fstT (sndT modu) in Is_refining_M mu'.
proof: Proof. intros mu alpha H_r. set (smodu:=semantic_modulus_h mu alpha H_r). set (n:=projS1 smodu). set (d':=(proj1_sig (projT2 smodu))). assert (Hn:n=(projT1 smodu)); trivial. assert (Hd':d'=(proj1_sig (projT2 smodu))); trivial. assert (H_depth: depth_h mu alpha (Is_refining_M_emits_h mu alpha H_r) = n);[apply (Is_refining_M_depth_h n _ alpha H_r Hn)|]. destruct (depth_h_modulus_h mu alpha (Is_refining_M_emits_h mu alpha H_r) n (Is_refining_M_depth_h n _ _ _ Hn)) as [d Hd]. destruct (proj2_sig (projS2 smodu)) as [H_Incl _]. rewrite Hd; simpl. apply Incl_M_absorbs_Is_refining_M. destruct (depth_h_Incl_M_inf_strong_general _ _ (Is_refining_M_emits_h mu alpha H_r) n H_depth) as [d'' [Hd''1 Hd''2]]. revert Hd''2. rewrite Hd; simpl. intros Hd''2. subst d''. assumption. Qed.
imports: QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit homographic hcorrectness Refining_M Bounded_M Incl_M