proposition: Lemma Lim_pres_less : forall (IR : CReals) (g h : R_COrdField IR), g[<]h -> Lim g[<]Lim h.
proof: Proof. do 3 intro. intro H. apply plus_cancel_less with (z := [--](Lim g)). astepl ([0]:IR). astepr (Lim h[-]Lim g). simpl in H. red in H. case H. intro N. intro H0. case H0. intros e H1 H3. set (H2 := True) in *. cut (SeqLimit (CS_seq IR g) (Lim g)). intro H4. cut (SeqLimit (CS_seq IR h) (Lim h)). intro H5. red in H4. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]ThreeNZ) (CS_seq IR g m[-]Lim g)}. intro H6. red in H5. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]ThreeNZ) (CS_seq IR h m[-]Lim h)}. intro H7. case H6. intro N1. intro H8. case H7. intro N2. intro H9. cut (AbsSmall (e [/]ThreeNZ) (CS_seq IR g (N + (N1 + N2))[-]Lim g)). intro H10. cut (AbsSmall (e [/]ThreeNZ) (CS_seq IR h (N + (N1 + N2))[-]Lim h)). intro H11. elim H10. intros H12 H13. elim H11. intros H14 H15. apply less_leEq_trans with (y := e [/]ThreeNZ). apply pos_div_three. assumption. rstepr (Lim h[-]CS_seq IR h (N + (N1 + N2))[+] (CS_seq IR h (N + (N1 + N2))[-]CS_seq IR g (N + (N1 + N2)))[+] (CS_seq IR g (N + (N1 + N2))[-]Lim g)). rstepl ([--](e [/]ThreeNZ)[+]e[+][--](e [/]ThreeNZ)). apply plus_resp_leEq_both. apply plus_resp_leEq_both. rstepr ([--](CS_seq IR h (N + (N1 + N2))[-]Lim h)). apply inv_resp_leEq. assumption. apply H3. apply Nat.le_add_r. assumption. apply H9. rewrite -> Nat.add_comm with (m := N2). rewrite -> Nat.add_shuffle3 with (m := N2). apply Nat.le_add_r. apply H8. rewrite -> Nat.add_shuffle3 with (m := N1). apply Nat.le_add_r. apply H5. apply pos_div_three. assumption. apply H4. apply pos_div_three. assumption. apply Lim_Cauchy. apply Lim_Cauchy. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism