proposition: Lemma as_Moebius_L: forall mu r, denom_nonvanishing_M mu r -> ((-1)<=as_Moebius mu r<=1)%R-> as_Moebius (product LL mu) r= (((as_Moebius mu r)-1)/((as_Moebius mu r)+3))%R.
proof: Proof. intros ((a,b),(c,d)) r H_denom H_r. generalize (denom_nonvanishing_M_product _ _ _ Is_refining_M_L H_r H_denom); generalize H_denom H_r; clear H_denom H_r. unfold product, as_Moebius, denom_nonvanishing_M, map_digits, fst, snd. realify_Q ;auto; simpl. replace (2+1) with 3; [|ring]. intros H_denom Hr H_denom_product. assert (H_denom': a*r+b+(c*r+d)*3<>0); [apply Rmult_reg_nonzero_l with (1/2); stepl ((1/2*a+3/2*c)*r+(1/2*b+3/2*d)); trivial; field; auto|]. rewrite Rdiv_Rminus_Rmult; trivial. rewrite Rdiv_Rplus_Rmult; trivial. rewrite Rdiv_Rdiv_simplify; trivial. transitivity (((a * r + b - (c * r + d) * 1)*(1/2))/((a * r + b + (c * r + d) * 3)*(1/2))). apply (f_equal2 Rdiv); field; auto. apply Rdiv_Rmult_simplify; auto. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M