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