proposition: Lemma Incl_T_absorbs_Is_refining_T:forall xi d, Incl_T xi d -> Is_refining_T (m_product (inv_digit d) xi).
proof: Proof. intros xi [ | | ] H_Incl; unfold inv_digit; [ apply Incl_T_absorbs_Is_refining_T_L | apply Incl_T_absorbs_Is_refining_T_R | apply Incl_T_absorbs_Is_refining_T_M ]; assumption. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier