proposition: Lemma fun_lim_seq_integral : conv_fun_seq' a b Hab g G contg contG.
proof: Proof. assert (H : conv_norm_fun_seq _ _ _ _ _ contIf contIF). apply conv_fun_seq'_norm; assumption. intros e H0. elim (Archimedes (AbsIR (b[-]a) [/] _[//]pos_ap_zero _ _ H0)); intros k Hk. elim (H k); intros N HN. exists N; intros. assert (H2 : included (Compact (Min_leEq_Max x0 x)) (Compact Hab)). apply included2_compact; auto. simpl in |- *. apply leEq_wdl with (AbsIR (Integral (Continuous_I_minus _ _ _ _ _ (prim_lemma _ _ (contf n) x0 Hx0 _ (contin_imp_inc _ _ _ _ (contg n) _ Hx)) (prim_lemma _ _ contF x0 Hx0 _ (contin_imp_inc _ _ _ _ contG _ Hx))))). 2: apply AbsIR_wd; apply Integral_minus. eapply leEq_transitive. apply Integral_leEq_norm. apply leEq_transitive with (one_div_succ k[*]AbsIR (b[-]a)). apply mult_resp_leEq_both. apply positive_norm. apply AbsIR_nonneg. eapply leEq_transitive. 2: apply (HN n H1). apply leEq_Norm_Funct; intros. apply norm_bnd_AbsIR. apply H2; auto. apply compact_elements with Hab; auto. unfold one_div_succ, Snring in |- *. rstepl (AbsIR (b[-]a) [/] _[//]nring_ap_zero _ _ (sym_not_eq (O_S k))). apply shift_div_leEq. apply pos_nring_S. eapply shift_leEq_mult'. assumption. apply less_leEq; eapply leEq_less_trans. apply Hk. simpl in |- *. apply less_plusOne. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems