proposition: Lemma limit_of_Integral : conv_fun_seq'_IR J f F contf contF -> forall x y, included (Compact (Min_leEq_Max x y)) J -> forall Hxy Hf HF, Cauchy_Lim_prop2 (fun n => Integral (a:=x) (b:=y) (Hab:=Hxy) (F:=f n) (Hf n)) (Integral (Hab:=Hxy) (F:=F) HF).
proof: Proof. intros convF x y H. set (x0 := Min x y) in *. intros. assert (Hx0 : J x0). apply H; apply compact_inc_lft. assert (Hx0' : Compact Hxy x0). apply compact_inc_lft. set (g := fun n : nat => ( [-S-]contf n) x0 Hx0) in *. set (G := ( [-S-]contF) x0 Hx0) in *. unfold Integral in |- *; fold x0 in |- *. apply (Cauchy_Lim_minus (fun n : nat => integral _ _ _ _ (Integral_inc2 _ _ _ _ (Hf n))) (fun n : nat => integral _ _ _ _ (Integral_inc1 _ _ _ _ (Hf n)))); fold x0 in |- *. apply limit_of_integral with (Hf := fun n : nat => Integral_inc2 _ _ Hxy _ (Hf n)); auto. apply included_trans with (Compact (Min_leEq_Max x y)); Included. apply included_compact. apply compact_inc_lft. apply compact_Min_rht. apply limit_of_integral with (Hf := fun n : nat => Integral_inc1 _ _ Hxy _ (Hf n)); auto. apply included_trans with (Compact (Min_leEq_Max x y)); auto. apply included_compact. apply compact_inc_lft. apply compact_Min_lft. Qed.
imports: CoRN.ftc.MoreIntegrals CoRN.ftc.CalculusTheorems