proposition: Lemma maximum_eta_discriminant_nondecreasing: forall a b c d x, c<=Zero -> Bounded_M ((a,b),(c,d)) -> -Qone<= x -> x <=Qone -> as_Moebius_Q ((0/1,1/1),(c,d)) x <= Qone/(c+d).
proof: Proof. intros a b c d x Hc H_bounded Hx_l Hx_r. assert (Hdc:=Bounded_M_c_plus_d_nonzero _ _ _ _ H_bounded). assert (Hx_lr:(-1<= x <= 1 )%R); [realify_Q; intros; split; trivial|]. generalize ((Bounded_M_denom_nonvanishing_M _ H_bounded) x Hx_lr). unfold denom_nonvanishing_M, as_Moebius_Q, fst, snd; rationalify_R_goal; intros Hcxd. qZ_numerals. stepl (Qone/(c*x+d)); [|field; split; auto; apply Q_to_R_Qneq; assumption]. apply Q_to_R_Qle. assert (Hcxd':=Q_to_R_Qneq _ _ Hcxd). clear Hcxd. realify_Q_goal; trivial. realify_Q. intros H1 H2 H3 H4 H5. apply Rle_zero_Rminus. stepr (((1-x)*(-c))/((c*1+d)*(c*x+d)))%R; [|field; split; auto]. unfold Rdiv; repeat apply Rle_mult_nonneg_nonneg; try Fourier.fourier; apply Rlt_le; apply Rinv_pos; apply (Bounded_M_twice_pos _ _ _ _ x R1 H_bounded); auto; apply one_is_in_base_interval. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs