proposition: Lemma Lim_well_def : forall (IR : CReals) (g h : R_COrdField IR), g[=]h -> Lim g[=]Lim h.
proof: Proof. intros. apply SeqLimit_unique with (y := Lim g). red in |- *. intros e H0. cut (Not (g[#]h)). intro. cut (forall e : IR, [0][<]e -> {N : nat | forall m : nat, N <= m -> AbsSmall e (CS_seq IR g m[-]CS_seq IR h m)}). intro H2. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR g m[-]CS_seq IR h m)}. intro H3. cut (SeqLimit (CS_seq IR g) (Lim g)). intro H4. red in H4. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR g m[-]Lim g)}. intro H5. case H3. intro N1. intro H6. case H5. intro N2. intro H7. exists (N1 + N2). intros. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). rstepr (CS_seq IR h m[-]CS_seq IR g m[+](CS_seq IR g m[-]Lim g)). apply AbsSmall_plus. apply AbsSmall_minus. apply H6. apply Nat.le_trans with (m := N1 + N2). apply Nat.le_add_r. assumption. apply H7. apply Nat.le_trans with (m := N1 + N2). rewrite Nat.add_comm; apply Nat.le_add_r. assumption. apply H4. apply pos_div_two. assumption. apply Lim_Cauchy. apply H2. apply pos_div_two. assumption. intros. apply Eq_alt_2_1. assumption. assumption. apply eq_imp_not_ap. assumption. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism