proposition: Lemma Cauchy_cont_Lim : forall H : Cauchy_fun_seq a b Hab f contf, Continuous_I Hab (Cauchy_fun_seq_Lim _ _ _ _ contf H).
proof: Proof. intros. split. Included. intros e He. elim (H _ (pos_div_three _ _ He)); intros N HN. elim (contf N); intros incf contf'. elim (contf' _ (pos_div_three _ _ He)). intros d H0 H1. exists d. assumption. intros x y H2 H3 Hx Hy H4. cut (forall x y z w : IR, AbsIR (x[-]w) [=] AbsIR (x[-]y[+] (y[-]z) [+] (z[-]w))); intros. 2: apply AbsIR_wd; rational. eapply leEq_wdl. 2: apply eq_symmetric_unfolded; apply H5 with (y := Part _ _ (incf x H2)) (z := Part _ _ (incf y H3)). rstepr (e [/]ThreeNZ[+]e [/]ThreeNZ[+]e [/]ThreeNZ). eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. eapply leEq_transitive. apply triangle_IR. apply plus_resp_leEq_both. apply leEq_wdl with (AbsIR (Part _ _ Hx[-]Lim (Cauchy_const (Part _ _ (incf x H2))))). 2: apply AbsIR_wd; apply cg_minus_wd. 2: algebra. 2: apply eq_symmetric_unfolded; apply Lim_const. simpl in |- *. apply leEq_wdl with (AbsIR (Lim (Build_CauchySeq IR _ (Cauchy_minus (Build_CauchySeq _ _ (Cauchy_fun_real _ _ _ _ _ H x Hx)) (Cauchy_const (Part _ _ (incf x H2))))))). 2: apply AbsIR_wd; apply Lim_minus. eapply leEq_wdl. 2: apply Lim_abs. simpl in |- *. apply str_seq_leEq_so_Lim_leEq. exists N; intros. simpl in |- *. eapply leEq_wdl. apply (HN i N) with (x := x) (Hx := Hx); auto with arith. apply AbsIR_wd; rational. apply H1; assumption. apply leEq_wdl with (AbsIR (Lim (Cauchy_const (Part _ _ (incf y H3))) [-] Part (Cauchy_fun_seq_Lim _ _ _ _ _ H) y Hy)). 2: apply AbsIR_wd; apply cg_minus_wd. 2: apply eq_symmetric_unfolded; apply Lim_const. 2: algebra. simpl in |- *. apply leEq_wdl with (AbsIR (Lim (Build_CauchySeq IR _ (Cauchy_minus (Cauchy_const (Part _ _ (incf y H3))) (Build_CauchySeq _ _ (Cauchy_fun_real _ _ _ _ _ H y Hy)))))). 2: apply AbsIR_wd; apply Lim_minus. eapply leEq_wdl. 2: apply Lim_abs. simpl in |- *. apply str_seq_leEq_so_Lim_leEq. exists N; intros. simpl in |- *. eapply leEq_wdl. apply (HN N i) with (x := y) (Hx := Hy); auto. apply AbsIR_wd; rational. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval