proposition: Lemma lb_integral : forall c, (forall x, I x -> forall Hx, c [<=] F x Hx) -> c[*] (b[-]a) [<=] Integral F contF.
proof: Proof. intros. apply leEq_wdl 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)