proposition: Lemma less_pres_Lim : forall (IR : CReals) (g h : R_COrdField IR), Lim g[<]Lim h -> g[<]h.
proof: Proof. do 3 intro. intro H. simpl in |- *. red in |- *. cut (SeqLimit (CS_seq IR g) (Lim g)). intro H0. cut (SeqLimit (CS_seq IR h) (Lim h)). intro H1. red in H0. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((Lim h[-]Lim g) [/]ThreeNZ) (CS_seq IR g m[-]Lim g)}. intro H2. case H2. intro N1. intro H3. red in H1. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((Lim h[-]Lim g) [/]ThreeNZ) (CS_seq IR h m[-]Lim h)}. intro H4. case H4. intro N2. intro H5. exists (N1 + N2). exists ((Lim h[-]Lim g) [/]FourNZ). apply pos_div_four. apply shift_zero_less_minus. assumption. intros. cut (AbsSmall ((Lim h[-]Lim g) [/]ThreeNZ) (CS_seq IR h n[-]Lim h)). intro. cut (AbsSmall ((Lim h[-]Lim g) [/]ThreeNZ) (CS_seq IR g n[-]Lim g)). intro. elim H7. intros H9 H10. elim H8. intros H11 H12. apply leEq_transitive with ((Lim h[-]Lim g) [/]ThreeNZ). apply mult_cancel_leEq with (Twelve:IR). astepl (nring (R:=IR) 0); apply nring_less; auto with arith. rstepl ([0][+]Three[*](Lim h[-]Lim g)). rstepr (Lim h[-]Lim g[+]Three[*](Lim h[-]Lim g)). apply plus_resp_leEq. apply shift_zero_leEq_minus; apply less_leEq; auto. apply plus_cancel_leEq_rht with (z := Lim g[-]Lim h). rstepr (CS_seq IR h n[-]Lim h[+](Lim g[-]CS_seq IR g n)). rstepl ([--]((Lim h[-]Lim g) [/]ThreeNZ)[+][--]((Lim h[-]Lim g) [/]ThreeNZ)). apply plus_resp_leEq_both. assumption. rstepr ([--](CS_seq IR g n[-]Lim g)). apply inv_resp_leEq. assumption. 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 H1. apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. assumption. apply H0. apply div_resp_pos. apply pos_three. apply shift_zero_less_minus. assumption. apply Lim_Cauchy. apply Lim_Cauchy. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism