proposition: Lemma Is_refining_T_modulus_q:forall xi alpha beta (H_r:Is_refining_T xi), let modu:=modulus_q xi alpha beta (Is_refining_T_emits_q xi alpha beta H_r) in let xi' := fstT (sndT modu) in Is_refining_T xi'.
proof: Proof. intros xi alpha beta H_r. set (smodu:=semantic_modulus_q xi alpha beta 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_q xi alpha beta (Is_refining_T_emits_q xi alpha beta H_r) = n);[apply (Is_refining_T_depth_q n _ alpha beta H_r Hn)|]. destruct (depth_q_modulus_q xi alpha beta (Is_refining_T_emits_q xi alpha beta H_r) n (Is_refining_T_depth_q n _ _ _ _ Hn)) as [d Hd]. destruct (proj2_sig (projS2 smodu)) as [H_Incl _]. rewrite Hd; simpl. apply Incl_T_absorbs_Is_refining_T. destruct (depth_q_Incl_T_inf_strong_general _ _ _ (Is_refining_T_emits_q xi alpha beta 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: Reals QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier digits ub LNP_Digit Refining_T Incl_T quadratic qcorrectness productivity_M