proposition: Lemma Bounded_M_auxiliary_6: forall c d r, d + c<=Zero -> d - c<=Zero ->(-1<=r<=1)%R->(c*r+d<=0)%R.
proof: Proof. intros c d r H1 H2 Hr. assert (Hd: d<=Zero); [apply Qmult_resp_Qle_pos_r with (Qone+Qone); auto; stepr Zero; auto; stepl ((d+c)+(d-c)); auto; ring|]. destruct (Qtrichotomy_inf Zero c) as [[Hc|Hc]|Hc]; realify_Q. intros; apply Bounded_M_neg_auxiliary_3; trivial. intros Hc _ _ Hd; rewrite <- Hc; stepl d; trivial; ring. intros; apply Bounded_M_neg_auxiliary_4; trivial. Qed.
imports: digits QArithSternBrocot(R_addenda) Fourier_solvable_ineqs Fourier Bounded_M