proposition: Lemma fun_Lim_seq_minus' : forall H H', conv_fun_seq' a b Hab (fun n => f n{-}g n) (F{-}G) H H'.
proof: Proof. intros H H' e H0. elim (convF _ (pos_div_two _ _ H0)); intros Nf HNf. elim (convG _ (pos_div_two _ _ H0)); intros Ng HNg. cut (Nf <= Nat.max Nf Ng); [ intro | apply Nat.le_max_l ]. cut (Ng <= Nat.max Nf Ng); [ intro | apply Nat.le_max_r ]. exists (Nat.max Nf Ng); intros. apply leEq_wdl with (AbsIR (Part _ _ (incf n x Hx) [-]Part _ _ (incg n x Hx) [-] (Part _ _ (incF x Hx) [-]Part _ _ (incG x Hx)))). 2: apply AbsIR_wd; simpl in |- *; algebra. apply leEq_wdl with (AbsIR (Part _ _ (incf n x Hx) [-]Part _ _ (incF x Hx) [-] (Part _ _ (incg n x Hx) [-]Part _ _ (incG x Hx)))). 2: apply AbsIR_wd; simpl in |- *; rational. rstepr (e [/]TwoNZ[+]e [/]TwoNZ). eapply leEq_transitive. apply triangle_IR_minus. apply plus_resp_leEq_both. unfold incf in |- *; apply HNf; apply Nat.le_trans with (Nat.max Nf Ng); auto. unfold incg in |- *; apply HNg; apply Nat.le_trans with (Nat.max Nf Ng); auto. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval