proposition: Lemma Cauchy_fun_seq'_seq : Cauchy_fun_seq' -> Cauchy_fun_seq.
proof: Proof. intro H. red in |- *; red in H. intros e He. elim (Archimedes ([1][/] e[//]pos_ap_zero _ _ He)). intros i Hei. cut ([0] [<] nring (R:=IR) i). intro Hi. elim (H i). intros N HN; exists N. intros. apply leEq_transitive with (one_div_succ (R:=IR) i). apply HN; assumption. unfold one_div_succ in |- *. rstepr ([1][/] _[//]recip_ap_zero _ _ (pos_ap_zero _ _ He)). unfold Snring in |- *. apply recip_resp_leEq. apply recip_resp_pos; assumption. apply less_leEq; apply leEq_less_trans with (nring (R:=IR) i). assumption. simpl in |- *; apply less_plusOne. apply less_leEq_trans with ([1][/] e[//]pos_ap_zero _ _ He). apply recip_resp_pos; assumption. assumption. Qed.
imports: CoRN.ftc.Continuity CoRN.ftc.PartInterval