proposition: Lemma as_Moebius_inv_R: forall mu r, denom_nonvanishing_M mu r -> (0 <= as_Moebius mu r <= 1)%R -> as_Moebius (product inv_RR mu) r = ((3 * as_Moebius mu r - 1) / (as_Moebius mu r + 1))%R.
proof: Proof. intros ((a,b),(c,d)) r H_denom H_r; generalize (denom_nonvanishing_M_product_inv_R _ _ H_denom H_r); generalize H_denom H_r; clear H_denom H_r; unfold product, as_Moebius, denom_nonvanishing_M, inv_RR, 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) * 1 <> 0); [apply Rmult_reg_nonzero_l with (1/2); stepl ((1/2*a+1/2*c)*r+(1/2*b+1/2*d)); trivial; field; auto|]. rewrite Rdiv_Rmult_numerator; trivial. repeat rewrite Rdiv_Rplus_Rmult; trivial. rewrite Rdiv_Rminus_Rmult; trivial. rewrite Rdiv_Rdiv_simplify; trivial. transitivity (((3 * (a * r + b) - (c * r + d) * 1)*(1/2))/(((a * r + b) + (c * r + d) * 1)*(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