proposition: Theorem SeqLimit_unique : forall (IR : CReals) (g : CauchySeq IR) (y : IR), SeqLimit g y -> y[=]Lim g.
proof: Proof. do 3 intro. intro H. apply not_ap_imp_eq. intro H0. case (ap_imp_less IR y (Lim g) H0). intro H1. red in H. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((Lim g[-]y) [/]ThreeNZ) (CS_seq IR g m[-]y)}. intro H2. case H2. intro N1. intro H3. cut (SeqLimit g (Lim g)). intro H4. red in H4. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((Lim g[-]y) [/]ThreeNZ) (CS_seq IR g m[-]Lim g)}. intro H5. case H5. intro N2. intro H6. apply less_irreflexive_unfolded with (x := y[-]Lim g). rstepr ([0][+](CS_seq _ g (N1 + N2)[-]Lim g)[+](y[-]CS_seq _ g (N1 + N2))). rstepl ((y[-]Lim g) [/]ThreeNZ[+](y[-]Lim g) [/]ThreeNZ[+](y[-]Lim g) [/]ThreeNZ). apply plus_resp_less_leEq. apply plus_resp_less_leEq. apply shift_div_less. apply pos_three. apply shift_minus_less; rstepr (Lim g); auto. elim (H6 (N1 + N2)); intros. rstepl ([--]((Lim g[-]y) [/]ThreeNZ)); auto. rewrite Nat.add_comm; apply Nat.le_add_r. elim (H3 (N1 + N2)); intros. apply inv_cancel_leEq. rstepr ((Lim g[-]y) [/]ThreeNZ); rstepl (g (N1 + N2)[-]y); auto. apply Nat.le_add_r. apply H4. apply pos_div_three. apply shift_zero_less_minus. assumption. apply Lim_Cauchy. apply H. apply pos_div_three. apply shift_zero_less_minus. assumption. intro. red in H. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((y[-]Lim g) [/]ThreeNZ) (CS_seq IR g m[-]y)}. intro H2. case H2. intro N1. intro H3. cut (SeqLimit g (Lim g)). intro H4. red in H4. cut {N : nat | forall m : nat, N <= m -> AbsSmall ((y[-]Lim g) [/]ThreeNZ) (CS_seq IR g m[-]Lim g)}. intro H5. case H5. intro N2. intros. apply less_irreflexive_unfolded with (x := Lim g[-]y). rstepr ([0][+](Lim g[-]CS_seq _ g (N1 + N2))[+](CS_seq _ g (N1 + N2)[-]y)). rstepl ((Lim g[-]y) [/]ThreeNZ[+](Lim g[-]y) [/]ThreeNZ[+](Lim g[-]y) [/]ThreeNZ). apply plus_resp_less_leEq. apply plus_resp_less_leEq. apply shift_div_less. apply pos_three. apply shift_minus_less; rstepr y; auto. elim (a (N1 + N2)); intros. apply inv_cancel_leEq. rstepr ((y[-]Lim g) [/]ThreeNZ); rstepl (g (N1 + N2)[-]Lim g); auto. rewrite Nat.add_comm; apply Nat.le_add_r. elim (H3 (N1 + N2)); intros. rstepl ([--]((y[-]Lim g) [/]ThreeNZ)); auto. apply Nat.le_add_r. apply H4. apply pos_div_three. apply shift_zero_less_minus. assumption. apply Lim_Cauchy. apply H. apply pos_div_three. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.Q_dense CoRN.reals.R_morphism