proposition: Lemma denom_nonvanishing_M_product_inv_L: forall mu r, denom_nonvanishing_M mu r -> ((-1) <= as_Moebius mu r <= 0)%R -> denom_nonvanishing_M (product inv_LL mu) r.
proof: Proof. intros ((a,b),(c,d)) r. unfold product, as_Moebius, denom_nonvanishing_M, inv_LL, fst, snd. intros H_denom [Hr1 Hr2]. destruct (Q_eq_dec c a) as [Hca|Hca]. destruct (Q_eq_dec d b) as [Hbd|Hbd]. apply False_ind; subst c d; apply (Rlt_irrefl 1); apply Rle_lt_trans with 0; trivial; stepl ((a * r + b)/(a * r + b)); trivial; field; trivial. subst c; stepl ((1%Z/2%Z)*(d-b)). apply Rmult_resp_nonzero; realify_Q; auto; apply Rminus_eq_contra; apply Q_to_R_not_eq; trivial. realify_Q_goal; auto; change (IZR (Zneg xH)) with (- IZR (Zpos xH))%R; field; auto. realify_Q; auto. intros Hca. generalize (Rminus_eq_contra _ _ Hca); clear Hca; intro Hca. 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 Rle_lt_trans with 0; trivial. stepl ((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_Rdiv_Rone; trivial; ring. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M