proposition: Lemma denom_nonvanishing_T_left_right_product: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 -> denom_nonvanishing_T (right_product (left_product xi mu1) mu2) r1 r2.
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) ((A',B'),(C',D')) r1 r2. unfold as_Tensor, as_Moebius, denom_nonvanishing_M, denom_nonvanishing_T, right_product, left_product, fst, snd. intros H_denom1 H_denom2 Hr1 Hr2 H_refining. realify_Q_goal. stepl (e*(A*r1+B)*(A'*r2+B') + f*(A*r1+B)*(C'*r2+D') + g*(C*r1+D)*(A'*r2+B') + h*(C*r1+D)*(C'*r2+D')); [|ring]. apply Rbilinear_non_zero_2; auto. apply (Is_refining_T_denom_nonvanishing_T _ _ _ H_refining Hr1 Hr2). Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier