proposition: Lemma f_pres_Lim : fun_pres_Lim R1 R2 f.
proof: Proof. red in |- *. intros. rename X into H. unfold Cauchy_Lim_prop2 in |- *. intros e2 H0. red in f_surj. unfold Cauchy_Lim_prop2 in H. cut {x : R1 | e2[=]f x}. intro H4. case H4. intros e1 H5. cut {N : nat | forall m : nat, N <= m -> AbsSmall e1 (a m[-]l_a)}. intro H6. case H6. intro N. intros. exists N. intros. cut (AbsSmall e1 (a m[-]l_a)). intro. elim H8. intros. astepl (f e1). astepr (f (a m[-]l_a)). split. astepl (f [--]e1). apply f_pres_leEq. assumption. assumption. apply f_pres_minus. assumption. apply f_pres_leEq. assumption. assumption. apply f_pres_min. assumption. apply a0. assumption. apply H. apply less_pres_f. assumption. astepl ([0]:R2). astepr e2. assumption. apply eq_symmetric_unfolded. apply f_pres_One. assumption. apply f_surj. Qed.
imports: CoRN.reals.CReals