proposition: Lemma compose_pres_Lim : fun_pres_Lim R1 R3 compose.
proof: Proof. red in |- *. unfold compose in |- *. case f. intro f_. intros f_1 f_2 f_3 f_4 f_5. case g. intro g_. intros g_1 g_2 g_3 g_4 g_5. intros. simpl in |- *. apply g_5 with (a := fun n : nat => f_ (a n)). apply f_5. assumption. Qed.
imports: CoRN.reals.CReals