proposition: Lemma Lim_pres_plus : forall (IR : CReals) (g h : R_COrdField IR), Lim (g[+]h)[=]Lim g[+]Lim h.
proof: Proof. intros. apply eq_symmetric_unfolded. apply SeqLimit_unique with (g := g[+]h). red in |- *. simpl in |- *. intros. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR g m[-]Lim g)}. intro H2. case H2. intro N1. intro H3. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR h m[-]Lim h)}. intro H4. case H4. intro N2. intro H5. exists (N1 + N2). intros. rstepr (CS_seq IR g m[-]Lim g[+](CS_seq IR h m[-]Lim h)). rstepl (e [/]TwoNZ[+]e [/]TwoNZ). apply AbsSmall_plus. apply H3. apply Nat.le_trans with (m := N1 + N2). apply Nat.le_add_r. assumption. apply H5. apply Nat.le_trans with (m := N1 + N2). rewrite Nat.add_comm; apply Nat.le_add_r. assumption. apply (ax_Lim _ _ (crl_proof IR) h). apply pos_div_two. assumption. apply (ax_Lim _ _ (crl_proof IR) g). apply pos_div_two. assumption. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism