proposition: Lemma Cauchy_fun_real_IR : Cauchy_fun_seq_IR -> forall x Hx, Cauchy_prop (fun n => Part _ _ (Continuous_imp_inc _ _ (contf n) x Hx)).
proof: Proof. intros H x Hx. red in H. cut (included (compact_single x) J). intro H0. set (contf' := fun i : nat => included_imp_Continuous J (f i) (contf i) _ _ (leEq_reflexive _ x) H0) in *. apply Cauchy_prop_wd with (fun n : nat => Part (f n) x ((fun i : nat => contin_imp_inc _ _ (leEq_reflexive _ x) (f i) (contf' i)) n x (compact_single_prop x))). apply Cauchy_fun_real. unfold contf' in |- *; simpl in |- *; apply H. intro; simpl in |- *; algebra. apply compact_single_iprop; auto. Qed.
imports: CoRN.ftc.FunctSeries CoRN.ftc.MoreFunctions