proposition: Lemma UC_integral_pos : forall {R : ConstructiveReals} f a b (modF : forall eps:CRcarrier R, 0 < eps -> CRcarrier R) (fCont : UniformCont f modF) (leab : a <= b), (forall x, (a <= x /\ x <= b) -> 0 <= f x) -> 0 <= UC_integral f a b modF fCont leab.
proof: Proof. intros. rewrite <- (UC_integral_zero (fun _ => 0) a b (fun _ _ => 1) (UC_constant 0) leab). apply UC_integral_nonneg. exact H. intros. reflexivity. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont