proposition: Lemma Bounded_M_neg_auxiliary_1:forall c d r, d + c < 0 -> (0 < c)%R -> (-1 <= r <= 1)%R -> c*r+d<0.
proof: Proof. intros c d r Hdc Hc [Hr1 Hr2]; apply Rle_lt_trans with (d+c); trivial; stepr (c*(1)+d); [|ring]; apply Rplus_le_compat_r; apply Rfourier_le; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier