proposition: Lemma ub_Integral : a [#] b -> forall c, (forall x, Compact Hab x -> forall Hx, AbsIR (F x Hx) [<=] c) -> forall x, Compact Hab x -> forall Hx, AbsIR (F x Hx) [<] c -> AbsIR (Integral contF) [<] c[*]AbsIR (b[-]a).
proof: Proof. intros H c H0 x H1 Hx H2. set (N := Norm_Funct contF) in *. cut (N [<=] c); intros. elim (less_cotransitive_unfolded _ _ _ H2 N); intros. apply less_leEq_trans with (N[*]AbsIR (b[-]a)). unfold N in |- *; apply Integral_less_norm with x Hx; auto. apply mult_resp_leEq_rht; auto. apply AbsIR_nonneg. apply leEq_less_trans with (N[*]AbsIR (b[-]a)). unfold N in |- *; apply Integral_leEq_norm. apply mult_resp_less; auto. apply AbsIR_pos. apply minus_ap_zero. apply ap_symmetric_unfolded; auto. unfold N in |- *; apply leEq_Norm_Funct; auto. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions