proposition: Lemma Is_refining_M_denom_nonvanishing_M:forall mu r, Is_refining_M mu -> ((-1)<=r<=1)%R -> denom_nonvanishing_M mu r.
proof: Proof. intros ((a,b),(c,d)) r H_refining Hr; generalize (Is_refining_M_d_minusplus_c_sign_dec _ _ _ _ H_refining); clear H_refining. intros [[_[_[_[_[H1 [H2 H3]]]]]]|[_[_[_[_[H1 [H2 H3]]]]]]]; red; simpl; realify_Q; intros H1 H2 H3; destruct (Qtrichotomy_inf Zero c) as [[Hc|Hc]|Hc]; realify_Q; intros Hc. apply Rlt_not_eq'; apply Bounded_M_pos_auxiliary_1; trivial... rewrite <- Hc; stepl d; auto; ring... apply Rlt_not_eq'; apply Bounded_M_pos_auxiliary_2; trivial... apply Rlt_not_eq; apply Bounded_M_neg_auxiliary_1; trivial... rewrite <- Hc; stepl d; auto; ring... apply Rlt_not_eq; apply Bounded_M_neg_auxiliary_2; trivial... Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M