proposition: Lemma lim_not_in_ranf : forall (n : nat), f_lim [#] (f n).
proof: Proof. intros. elim (f_n_not_in_int n); intros. assert (f n [<] f_lim). apply less_leEq_trans with (seq1_lft n); auto. apply lim_bigger. apply ap_symmetric. apply less_imp_ap; auto. assert (f_lim [<] f n). apply leEq_less_trans with (seq1_rht n); auto. apply lim_smaller. apply less_imp_ap; auto. Qed.
imports: CoRN.reals.CReals1