proposition: Lemma Bounded_M_pos: forall a b c d r, Bounded_M ((a,b),(c,d))-> Zero<d ->(-1<=r<=1)%R->(0<c*r+d)%R.
proof: Proof. intros a b c d r [[H1 H2]|[H1 H2]] Hd Hr; unfold fst, snd in H1; unfold fst, snd in H2. destruct (Qtrichotomy_inf Zero c) as [[Hc|Hc]|Hc]. generalize (Q_to_Rlt _ _ H2) (Q_to_Rlt _ _ Hc) Hr; clear H1 H2 Hc Hr; rewrite Q_to_R_Zero; try rewrite Q_to_Rplus; try rewrite Q_to_Rminus; intros; apply Bounded_M_pos_auxiliary_1; trivial... rewrite <- Hc; generalize (Q_to_Rlt _ _ Hd); clear Hd; rewrite Q_to_R_Zero; intro Hd; stepr d; trivial; ring... generalize (Q_to_Rlt _ _ H1) (Q_to_Rlt _ _ Hc) Hr; clear H1 H2 Hc Hr; rewrite Q_to_R_Zero; try rewrite Q_to_Rplus; try rewrite Q_to_Rminus; intros; apply Bounded_M_pos_auxiliary_2; trivial... apply False_ind; apply Qlt_irreflexive with Zero; apply Qlt_transitive with (d+d); auto; stepl ((d+c)+(d-c)); auto; ring. Qed.
imports: digits Raxioms RIneq QArithSternBrocot(R_addenda) Fourier_solvable_ineqs