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