proposition: Lemma limit_comp : forall f g Df Dg l l' z, limit1_in f Df l z -> limit1_in g Dg l' l -> limit1_in (fun z => g (f z)) (Dgf Df Dg f) l' z.
proof: Proof. unfold limit1_in, limit_in, Dgf in |- *; simpl in |- *. intros f g Df Dg l l' x0 Hf Hg eps eps_pos. elim (Hg eps eps_pos). intros alpg lg. elim (Hf alpg). 2: tauto. intros alpf lf. exists alpf. intuition. Qed.
imports: Rlimit Cbase Ctacfield Cnorm Cprop_base Rsequence_def Csequence Csequence_facts Cfunctions