proposition: Lemma as_Tensor_right_left_product_as_Moebius:forall xi mu1 mu2 r1 r2, denom_nonvanishing_M mu1 r1->denom_nonvanishing_M mu2 r2 -> ((-1)<=as_Moebius mu1 r1<=1)%R -> ((-1)<=as_Moebius mu2 r2<=1)%R -> Is_refining_T xi -> as_Tensor (right_product (left_product xi mu1) mu2) r1 r2= as_Tensor xi (as_Moebius mu1 r1) (as_Moebius mu2 r2).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) ((A',B'),(C',D')) r1 r2 H_denom1 H_denom2 H_mu_r1 H_mu_r2 H_refining. generalize (denom_nonvanishing_T_left_right_product _ _ _ _ _ H_denom1 H_denom2 H_mu_r1 H_mu_r2 H_refining). generalize H_denom1 H_denom2; clear H_denom1 H_denom2. unfold as_Tensor, as_Moebius, denom_nonvanishing_M, denom_nonvanishing_T, right_product, left_product, fst, snd. realify_Q. intros H_denom1 H_denom2 H_denom_prod. generalize (Rmult_resp_nonzero _ _ H_denom1 H_denom2); intros H_denom3. rewrite (Rmult_assoc a); rewrite (Rmult_assoc e). rewrite Rdiv_Rmult_numerator_denominator; trivial. repeat rewrite Rdiv_Rmult_numerator; auto. repeat rewrite Rplus_Rdiv; auto. repeat rewrite Rdiv_Rplus_Rmult; auto. rewrite Rdiv_Rdiv_simplify; auto. rewrite <- (Rdiv_Rmult_simplify (((a * A + c * C) * A' + (b * A + d * C) * C') * r1 * r2 + ((a * A + c * C) * B' + (b * A + d * C) * D') * r1 + ((a * B + c * D) * A' + (b * B + d * D) * C') * r2 + ((a * B + c * D) * B' + (b * B + d * D) * D')) _ _ H_denom3 H_denom_prod). apply (f_equal2 Rdiv); ring. stepl ((C*r1+D)*(C'*r2+D')* (((e*A+g*C)*A'+(f*A+h*C)*C')*r1*r2+((e*A+g*C)*B'+(f*A+h*C)*D')*r1+ ((e*B+g*D)*A'+(f*B+h*D)*C')*r2+((e*B+g*D)*B'+(f*B+h*D)*D'))); auto; ring. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier