proposition: Lemma ub_integral : forall c, (forall x, I x -> forall Hx, F x Hx [<=] c) -> Integral F contF [<=] c[*] (b[-]a).
proof: Proof. intros. apply leEq_wdr with (Integral _ (Continuous_I_const a b Hab c)). 2: apply integral_const. apply monotonous_integral. simpl in |- *; auto. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)