proposition: Lemma denom_nonvanishing_T_m_product:forall xi mu r1 r2, Is_refining_M mu ->((-1)<=as_Tensor xi r1 r2<=1) -> denom_nonvanishing_T xi r1 r2-> denom_nonvanishing_T (m_product mu xi) r1 r2.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) r1 r2 H_refining. unfold as_Tensor, denom_nonvanishing_M, denom_nonvanishing_T, m_product, fst, snd. intros Hr H_denom. realify_Q_goal. stepl (C *(a * r1 * r2 + b * r1 + c * r2 + d)+D*(e * r1 * r2 + f * r1 + g * r2 + h)); [|ring]. apply Rlinear_non_zero_2; auto. apply (Is_refining_M_denom_nonvanishing_M _ _ H_refining Hr). Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier