proposition: Lemma Is_refining_T_Bounded_T_left_right_product:forall xi mu1 mu2, Is_refining_M mu1 -> Is_refining_M mu2 -> Bounded_T xi -> Bounded_T (right_product (left_product xi mu1) mu2).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) ((A',B'),(C',D')) H_refining1 H_refining2 H_bounded. apply denom_nonvanishing_T_Bounded_T; intros r1 r2 Hr1 Hr2. assert (H_mu1:=Is_refining_M_property _ r1 Hr1 H_refining1); assert (H_mu2:=Is_refining_M_property _ r2 Hr2 H_refining2). generalize (Bounded_T_denom_nonvanishing_T _ H_bounded _ _ H_mu1 H_mu2). unfold as_Moebius, denom_nonvanishing_T, right_product, left_product, fst, snd. intros H_denom. 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_M_denom_nonvanishing_M _ _ H_refining1 Hr1). apply (Is_refining_M_denom_nonvanishing_M _ _ H_refining2 Hr2). Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier