proposition: Lemma RInt_le_l (l : R) : (forall x : R, ra <= x <= rb -> l <= f x) -> l <= RInt f ra rb / (rb - ra).
proof: Proof. intros Hf. apply Rle_div_r. now apply Rgt_minus. rewrite Rmult_comm, <- (RInt_const (V := R_CompleteNormedModule)). apply RInt_le with (3 := Hint). now apply Rlt_le. apply ex_RInt_const. intros x [Hx1 Hx2]. apply Hf. split; now apply Rlt_le. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux) Coquelicot.Coquelicot