proposition: Lemma Bounded_T_Incl_T_M_folded: forall xi, Bounded_T xi -> (forall r1 r2,(-1 <= r1 <= 1)%R -> (-1 <= r2 <= 1)%R -> ((-1/3)<= as_Tensor xi r1 r2 <= 1/3)%R) -> Incl_T xi MM.
proof: Proof. intros xi H_bound; generalize (Bounded_T_denom_nonvanishing_T xi H_bound); apply Incl_T_M_folded. Qed.
imports: digits Bounded_M Bounded_T Incl_M Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs