proposition: Lemma Rint_pos : forall f a b x, a <= b -> (forall u, a <= u <= b -> 0 <= f u) -> Rint f a b x -> 0 <= x.
proof: Proof. intros f a b x Hab Hpos Hf. destruct(Rint_constant 0 a b) as [pr0 H0]. ring_simplify in H0. apply Rint_le_compat with (fct_cte 0) f a b. apply Hab. intros u Hu; apply Hpos; intuition. exists pr0. apply H0. apply Hf. Qed.
imports: Reals RiemannInt RIneq Lra R_sqr MyRfunctions