proposition: Lemma fun_Lim_seq_inv : forall H H', conv_fun_seq' a b Hab (fun n => {--} (f n)) {--} (Cauchy_fun_seq_Lim _ _ _ _ _ Hf) H H'.
proof: Proof. intros. cut (forall n : nat, Continuous_I Hab ( [-C-][0]{-}f n)). intro H0. unfold I in |- *; eapply conv_fun_seq'_wdl with (fun n : nat => [-C-][0]{-}f n) H0 H'. intro H1; FEQ; try (apply contin_imp_inc; apply contf). cut (Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ _ (fun_Cauchy_prop_const a b Hab [-C-][0] (Continuous_I_const _ _ _ _)) {-} Cauchy_fun_seq_Lim _ _ _ _ _ Hf)). intros H1. apply conv_fun_seq'_wdr with H0 (Cauchy_fun_seq_Lim _ _ _ _ _ (fun_Cauchy_prop_const a b Hab [-C-][0] (Continuous_I_const _ _ _ _)) {-} Cauchy_fun_seq_Lim _ _ _ _ _ Hf) H1. apply eq_imp_Feq. Included. Included. intros; simpl in |- *. astepr ([0][-]Lim (Build_CauchySeq _ _ (Cauchy_fun_real _ _ _ _ contf Hf x Hx'))). apply cg_minus_wd. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Lim_const. apply Lim_wd'; intros; simpl in |- *; algebra. apply Lim_wd'; intros; simpl in |- *; rational. apply fun_Lim_seq_minus with (f := fun n : nat => [-C-][0]:PartIR). Contin. Contin. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval