proposition: Lemma Bounded_M_pos_auxiliary_3:forall c d r, 0 <= d - c -> (0 < c)%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 Rfourier_le; trivial. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier