proposition: Lemma fun_Lim_seq_comp' : forall H H', conv_fun_seq' a b Hab (fun n => g n[o]f n) (G[o]F) H H'.
proof: Proof. intros H H'. intros e He. destruct (convG _ (pos_div_two _ _ He)) as [N HN]. destruct (CAnd_proj2 _ _ contG _ (pos_div_two _ _ He)) as [z Hz Hz0]. destruct (convF _ Hz) as [M HM]. exists (Nat.max N M). intros n Hn x Hx. assert (Hn0 : N <= n). apply Nat.le_trans with (Nat.max N M); auto with *. assert (Hn1 : M <= n). apply Nat.le_trans with (Nat.max N M); auto with *. apply AbsSmall_imp_AbsIR. assert (X:Continuous_I (a:=a) (b:=b) Hab (G[o]f n)). eapply Continuous_I_comp. apply contf. apply contG. (split; try assumption). apply (rangef n). rstepr (((g n[o]f n) x (contin_imp_inc a b Hab (g n[o]f n) (H n) x Hx)[-] ((G[o]f n) x (contin_imp_inc a b Hab _ X x Hx)))[+] (((G[o]f n) x (contin_imp_inc a b Hab _ X x Hx))[-] (G[o]F) x (contin_imp_inc a b Hab (G[o]F) H' x Hx))). apply AbsSmall_eps_div_two. apply AbsIR_imp_AbsSmall. simpl (AbsIR ((g n[o]f n) x (contin_imp_inc a b Hab (g n[o]f n) (H n) x Hx)[-] (G[o]f n) x (contin_imp_inc a b Hab (G[o]f n) X x Hx))). generalize (ProjT1 (contin_imp_inc a b Hab (g n[o]f n) (H n) x Hx)) (ProjT1 (contin_imp_inc a b Hab (G[o]f n) X x Hx)) (ProjT2 (contin_imp_inc a b Hab (g n[o]f n) (H n) x Hx)) (ProjT2 (contin_imp_inc a b Hab (G[o]f n) X x Hx)). intros Y0 Y1 Y2 Y3. assert (fnx := pfwdef _ _ _ _ Y0 Y1 (eq_reflexive _ x)). assert (Y4 : Dom (g n) (f n x Y1)). apply (dom_wd _ (g n) (f n x Y0));assumption. stepl (ABSIR (g n (f n x Y1) Y4[-]G (f n x Y1) Y3)); [| apply AbsIR_wd; rational]. generalize (rangef n x Y1 Hx). generalize (f n x Y1) Y4 Y3. clear Y0 Y1 Y2 Y3 fnx Y4. intros y Hy0 Hy1 Hy. stepl (ABSIR (g n y (contin_imp_inc c d Hcd (g n) (contg n) y Hy)[-] G y (contin_imp_inc c d Hcd G contG y Hy))); [| apply AbsIR_wd; rational]. apply HN. assumption. apply AbsIR_imp_AbsSmall. simpl. apply Hz0. apply rangef; assumption. apply rangeF; assumption. stepl (AbsIR (f n x (contin_imp_inc a b Hab (f n) (contf n) x Hx)[-] F x (contin_imp_inc a b Hab F contF x Hx))); [| apply AbsIR_wd; rational]. apply HM. assumption. Qed.
imports: CoRN.ftc.MoreFunctions CoRN.ftc.MoreFunSeries