proposition: Lemma as_Tensor_M: forall xi r1 r2, denom_nonvanishing_T xi r1 r2 -> ((-1)<=as_Tensor xi r1 r2<=1)%R-> as_Tensor (m_product MM xi) r1 r2 = ((as_Tensor xi r1 r2)/3)%R.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) r1 r2 H_denom H_r; generalize (denom_nonvanishing_T_m_product _ _ _ _ Is_refining_M_M H_r H_denom); generalize H_denom; clear H_denom H_r; unfold m_product, as_Tensor, denom_nonvanishing_M, denom_nonvanishing_T, map_digits, fst, snd; realify_Q ;auto; simpl; replace (2+1) with 3; [|ring]; intros H_denom H_denom_product. rewrite Rdiv_Rdiv_Rmult_numerator; auto. apply (f_equal2 Rdiv); field; auto. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier