proposition: Lemma integral_leEq_norm : AbsIR (Integral F contF) [<=] Norm_Funct contF[*] (b[-]a).
proof: Proof. simpl in |- *; unfold ABSIR in |- *. apply Max_leEq. apply ub_integral. intros; eapply leEq_transitive. apply leEq_AbsIR. unfold I in |- *; apply norm_bnd_AbsIR; assumption. astepr ( [--][--] (Norm_Funct contF[*] (b[-]a))). astepr ( [--] ( [--] (Norm_Funct contF) [*] (b[-]a))). apply inv_resp_leEq. apply lb_integral. intros; astepr ( [--][--] (Part F x Hx)). apply inv_resp_leEq. eapply leEq_transitive. apply inv_leEq_AbsIR. unfold I in |- *; apply norm_bnd_AbsIR; assumption. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)