proposition: Lemma Is_refining_T_left_right_product:forall xi mu_l mu_r, Is_refining_T xi -> Is_refining_M mu_l -> Is_refining_M mu_r -> Is_refining_T (right_product (left_product xi mu_l) mu_r).
proof: Proof. intros (((a,b),(c,d)),((e,f),(g,h))) ((A,B),(C,D)) ((A',B'),(C',D')) H_xi H_l H_r. apply Is_refining_T_property_fold; intros r1 r2 Hr1 Hr2. apply denom_nonvanishing_T_left_right_product; trivial; [ apply Is_refining_M_denom_nonvanishing_M | apply Is_refining_M_denom_nonvanishing_M | apply Is_refining_M_property | apply Is_refining_M_property ]; trivial. rewrite as_Tensor_right_left_product_as_Moebius; trivial; repeat apply Is_refining_M_property; trivial; repeat apply Is_refining_M_denom_nonvanishing_M; trivial; apply Is_refining_T_property; trivial; repeat apply Is_refining_M_property; trivial. Qed.
imports: digits Refining_M Bounded_T QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier