proposition: Lemma denom_nonvanishing_M_product_inv_R: forall mu r, denom_nonvanishing_M mu r -> (0 <= as_Moebius mu r <= 1)%R -> denom_nonvanishing_M (product inv_RR mu) r.
proof: Proof. intros ((a,b),(c,d)) r. unfold product, as_Moebius, denom_nonvanishing_M, inv_RR, fst, snd. intros H_denom [Hr1 Hr2]. destruct (Q_eq_dec c (Qopp a)) as [Hca|Hca]. destruct (Q_eq_dec d (Qopp b)) as [Hbd|Hbd]. apply False_ind; subst c d; apply (Rlt_irrefl (-1)); apply Rlt_le_trans with 0; trivial; stepr ((a * r + b)/((-a)%Q * r + (-b)%Q)); trivial; generalize H_denom; clear H_denom; realify_Q; intros H_denom; field; trivial. subst c; stepl ((1%Z/2%Z)*(d+b)). apply Rmult_resp_nonzero; realify_Q; auto; intros Hbd; stepl (d-(-b)); [|ring]; apply Rminus_eq_contra; trivial. realify_Q; auto; intros Hdb; field; auto. realify_Q; auto; intros Hca. assert (Hca': c + a <> 0); [stepl (c-(-a));[|ring]; apply Rminus_eq_contra; assumption|]. change (IZR 1) with 1; change (IZR (-1)) with (-1); change (IZR 2) with 2. stepl (1/2*((c+a)*r+(d+b))); [|field; auto]. apply Rmult_resp_nonzero; auto. apply Rlinear_non_zero_3; trivial. intro H_false. apply (Rlt_irrefl (-1)). apply Rlt_le_trans with 0; trivial. stepr ((a * r + b)/(c * r + d)); trivial. subst r. repeat rewrite Rdiv_Rmult_numerator; trivial. repeat rewrite Rdiv_Rplus_Rmult; trivial. assert (H_linear:c * - (d + b) + (c + a) * d<>0);[rewrite (Rmult_comm (c+a) d); apply Rlinear_non_zero_2; trivial|]. rewrite Rdiv_Rdiv_simplify; trivial. apply Req_Ropp_Rdiv_minus_Rone; trivial; ring. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M