proposition: Lemma funseq_conv : forall J x y, nonvoid J -> conv_fun_seq'_IR J (seq_to_funseq x) [-C-]y (fun n => Continuous_const _ _) (Continuous_const _ _) -> Cauchy_Lim_prop2 x y.
proof: Proof. intros J x y H H0 eps H1. elim (nonvoid_point J H); intros x0 Hx0. cut (included (compact_single x0) J). 2: apply compact_single_iprop; auto. intro H2. elim (H0 _ _ (leEq_reflexive _ _) H2 eps). intros N HN. exists N; intros. simpl in HN. apply AbsIR_imp_AbsSmall. apply HN with x0. auto. fold (compact_single x0) in |- *. apply compact_single_prop. auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions