proposition: Lemma limit_comp : forall (f g:R -> R) (Df Dg:R -> Prop) (l l' x0:R), limit1_in f Df l x0 -> limit1_in g Dg l' l -> limit1_in (fun x:R => g (f x)) (Dgf Df Dg f) l' x0.
proof: Proof. unfold limit1_in, limit_in, Dgf; simpl. 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: Rbase Rfunctions Lra