proposition: Lemma has_limit_sum : forall f g: nat->U, has_lim f -> has_lim g -> has_lim (fun x => f x + g x).
proof: Proof. unfold has_lim; intros. apply Ole_trans with (limsup f + limsup g); auto. apply Ole_trans with (liminf f + liminf g); auto. Qed.
imports: ALEA(Utheory)