proposition: Lemma denom_nonvanishing_M_Bounded_M:forall mu, (forall r, (-1 <= r <= 1)%R -> denom_nonvanishing_M mu r) -> Bounded_M mu.
proof: Proof. intros ((a,b),(c,d)) H_denom. unfold denom_nonvanishing_M in H_denom; simpl in H_denom. assert (H_dcmin:d-c <>Zero); [apply Q_to_R_Qneq; realify_Q; stepl (c*(-1)+d)%R; [|ring]; apply (H_denom (-1)%R min_one_is_in_base_interval)|]. assert (H_dc:d+c <>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (c*1+d)%R; [|ring]; apply (H_denom (1)%R one_is_in_base_interval)|]. assert (Hd: d<>Zero); [apply Q_to_R_Qneq; realify_Q_goal; stepl (c*0+d)%R; [|ring]; apply H_denom; split; Fourier.fourier|]. unfold Incl_M, Bounded_M, map_digits, fst, snd. destruct (Q_zerop c) as [Hc|Hc]. subst c; destruct (not_Qeq_inf _ _ Hd) as [Hd_sg|Hd_sg]. right; split; stepl d; trivial; ring. left; split; stepr d; trivial; ring. destruct (Q_le_lt_dec (-Qone) (- (d/c))) as [Hdc_min|Hdc_min]. destruct (Q_le_lt_dec (- (d/c)) (Qone)) as [Hdc_|Hdc_]. apply False_ind; apply (H_denom (-(d/c))%R); [ revert Hc; realify_Q_assumptions; intros _ _ _ H1 H2 H3; revert H2 H1; realify_Q_goal; tauto | try field; rationalify_R_goal; apply Q_to_R_not_eq; assumption ]... destruct (not_Qeq_inf _ _ Hc) as [Hc_sg|Hc_sg]. left; split. apply Qlt_Qdiv_denom_neg_neg with c; trivial; stepl (Qone-(-(d/c))); [| field; auto]; apply Qlt_Qminus_Zero_neg; assumption. apply Qlt_Qdiv_denom_neg_neg with c; trivial; stepl ((-Qone)-(-(d/c))); [| field; auto]; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with Qone; auto. right; split. apply Qlt_Qdiv_denom_pos_neg with c; trivial; stepl (Qone-(-(d/c))); [| field; auto]; apply Qlt_Qminus_Zero_neg; assumption. apply Qlt_Qdiv_denom_pos_neg with c; trivial; stepl ((-Qone)-(-(d/c))); [| field; auto]; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with Qone; auto... destruct (not_Qeq_inf _ _ Hc) as [Hc_sg|Hc_sg]. right; split. apply Qlt_pos_Qopp; apply Qlt_Qdiv_denom_neg_neg with c; trivial; stepl ((-(d/c))-(Qone)); [| field; auto]; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with (-Qone); auto. apply Qlt_pos_Qopp; apply Qlt_Qdiv_denom_neg_neg with c; trivial; stepl ((-(d/c))-(-Qone)); [| field; auto]; apply Qlt_Qminus_Zero_neg; assumption. left; split. apply Qlt_neg_Qopp; apply Qlt_Qdiv_denom_pos_neg with c; trivial. stepl ((-(d/c))-(Qone)); [| field; auto]; apply Qlt_Qminus_Zero_neg; apply Qlt_transitive with (-Qone); auto. apply Qlt_neg_Qopp; apply Qlt_Qdiv_denom_pos_neg with c; trivial; stepl ((-(d/c))-(-Qone)); [| field; auto]; apply Qlt_Qminus_Zero_neg; assumption. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs