proposition: Lemma Lim_one_one : forall (IR : CReals) (g h : R_COrdField IR), Lim g[=]Lim h -> g[=]h.
proof: Proof. intros. apply not_ap_imp_eq. apply Eq_alt_2_2 with (x := g) (y := h). intros. cut (SeqLimit (CS_seq IR g) (Lim g)). intro H1. red in H1. cut (SeqLimit (CS_seq IR h) (Lim h)). intro H2. red in H2. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR g m[-]Lim g)}. intro H3. cut {N : nat | forall m : nat, N <= m -> AbsSmall (e [/]TwoNZ) (CS_seq IR h m[-]Lim h)}. intro H4. case H3. intro N1. intro H5. case H4. intro N2. intro H6. exists (N1 + N2). intros m H7. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). astepr (CS_seq IR g m[-]Lim g[+](Lim h[-]CS_seq IR h m)). apply AbsSmall_plus. apply H5. apply Nat.le_trans with (m := N1 + N2). apply Nat.le_add_r. assumption. apply AbsSmall_minus. apply H6. apply Nat.le_trans with (m := N1 + N2). rewrite Nat.add_comm; apply Nat.le_add_r. assumption. apply eq_transitive_unfolded with (y := CS_seq IR g m[-]CS_seq IR h m[+](Lim h[-]Lim g)). rational. astepr (CS_seq IR g m[-]CS_seq IR h m[+][0]). apply bin_op_wd_unfolded. apply eq_reflexive_unfolded. apply cg_cancel_rht with (x := Lim g). apply eq_transitive_unfolded with (y := Lim h). apply eq_symmetric_unfolded. apply cg_cancel_mixed. astepr (Lim g). apply eq_symmetric_unfolded. assumption. apply H2. apply pos_div_two. assumption. apply H1. apply pos_div_two. assumption. apply Lim_Cauchy. apply Lim_Cauchy. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism