proposition: Lemma unique_MSseqLim : forall (X : CMetricSpace) (seq : nat -> X) (a b : X), MSseqLimit seq a and MSseqLimit seq b -> a[=]b.
proof: Proof. intros X seq a b. unfold MSseqLimit in |- *. simpl in |- *. intros H. apply d_zero_imp_eq. apply not_ap_imp_eq. red in |- *. intro H1. set (H2 := recip_ap_zero IR (a[-d]b) H1) in *. set (H3 := Archimedes' (OneR[/] a[-d]b[//]H1)) in *. elim H3. intros n H4. set (H6 := less_transitive_unfolded IR ([1][/] a[-d]b[//]H1) ( nring n) (nring n[+][1]) H4 (nring_less_succ IR n)) in *. elim H. intros H5 H7. elim (H5 (S (S n)) (ap_symmetric_unfolded IR [0] ([0][+][1][+][1]) (less_imp_ap IR [0] ([0][+][1][+][1]) (less_transitive_unfolded IR [0] ([0][+][1]) ( [0][+][1][+][1]) (less_plusOne IR [0]) (less_plusOne IR (ZeroR[+][1])))))). intros x H8. elim (H7 (S (S n)) (ap_symmetric_unfolded IR [0] ([0][+][1][+][1]) (less_imp_ap IR [0] ([0][+][1][+][1]) (less_transitive_unfolded IR [0] ([0][+][1]) ( [0][+][1][+][1]) (less_plusOne IR [0]) (less_plusOne IR ([0][+][1]:IR)))))). intros y H9. set (H10 := H9 (Nat.max y x)) in *. set (H11 := H8 (Nat.max x y)) in *. simpl in |- *. set (H12 := H11 (nz x y)) in *. set (H13 := H10 (nz y x)) in *. set (H14 := ap_symmetric_unfolded IR [0] ([0][+][1][+][1]) (less_imp_ap IR [0] ([0][+][1][+][1]) (less_transitive_unfolded IR [0] ([0][+][1]) ( [0][+][1][+][1]) (less_plusOne IR [0]) (less_plusOne IR ([0][+][1]))))) in *. cut ((seq (Nat.max x y)[-d]a)[+](seq (Nat.max y x)[-d]b)[<] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)[+] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)). intro H15. cut (nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)[+] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)[<=] (seq (Nat.max x y)[-d]a)[+](seq (Nat.max y x)[-d]b)). rewrite -> leEq_def in |- *. intro H16. auto. cut (nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)[+] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)[<=] a[-d]b). intro H16. apply leEq_transitive with (a[-d]b). exact H16. astepr ((seq (Nat.max x y)[-d]a)[+](seq (Nat.max x y)[-d]b)). astepr ((a[-d]seq (Nat.max x y))[+](seq (Nat.max x y)[-d]b)). apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. astepl ((seq (Nat.max x y)[-d]b)[+](a[-d]seq (Nat.max x y))). astepr ((seq (Nat.max x y)[-d]b)[+](seq (Nat.max x y)[-d]a)). apply plus_resp_eq. simpl in |- *. apply d_com. apply plus_resp_eq. apply d_wd. cut (Nat.max x y = Nat.max y x -> seq (Nat.max x y)[=]seq (Nat.max y x)). intro H17. apply H17. apply Nat.max_comm. intro H17. rewrite H17. apply eq_reflexive. astepl ((Two:IR)[*]nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)). astepl (nexp IR (S n) ([1][/] [0][+][1][+][1][//]H14)). astepl (([1][/] [0][+][1][+][1][//]H14)[^]S n). astepl ([1][/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H14). apply leEq_transitive with ([1][/] nring (S n)[//] ap_symmetric_unfolded IR [0] (nring (S n)) (less_imp_ap IR [0] (nring (S n)) (pos_Snring IR n))). apply leEq_transitive with ([1][/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H14). 2: apply less_leEq. 2: set (Hn := bin_less_un) in *. 2: generalize Hn. 2: simpl in |- *. 2: intro Hn'. 2: apply Hn'. apply recip_resp_leEq. apply nexp_resp_pos. astepr (Two:IR). apply pos_two. apply eq_imp_leEq. apply eq_reflexive_unfolded. apply shift_div_leEq. apply (pos_Snring IR n). apply shift_leEq_mult' with H1. 2: apply less_leEq. 2: apply H6. cut ([0][<]a[-d]b or a[-d]b[<][0]). intro H16. elim H16. intro H17. exact H17. intro H17. set (H18 := ax_d_nneg X (cms_d (c:=X))) in *. generalize H18. unfold nneg in |- *. intro H19. set (H20 := H19 (CPsMetricSpace_is_CPsMetricSpace X) a b) in *. rewrite -> leEq_def in H20. set (H21 := H20 H17) in *. intuition. apply ap_imp_less. apply ap_symmetric_unfolded. exact H1. astepl ((OneR[/] [0][+][1][+][1][//]H14)[^]S n). astepl (OneR[^]S n[/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H14). astepl (OneR[/] ([0][+][1][+][1])[^]S n[//]nexp_resp_ap_zero (S n) H14). astepl ((OneR[+][1])[*] ([1][/] ([0][+][1][+][1])[^]S (S n)[//]nexp_resp_ap_zero (S (S n)) H14)). apply mult_cancel_lft with (OneR[/] [0][+][1][+][1][//]H14). apply div_resp_ap_zero_rev. apply ap_symmetric_unfolded. apply less_imp_ap. apply pos_one. astepr (([1][/] [0][+][1][+][1][//]H14)[*]([0][+][1][+][1])[*] ([1][/] ([0][+][1][+][1])[^]S (S n)[//]nexp_resp_ap_zero (S (S n)) H14)). astepr (OneR[*] ([1][/] ([0][+][1][+][1])[^]S (S n)[//]nexp_resp_ap_zero (S (S n)) H14)). astepr (OneR[/] ([0][+][1][+][1])[^]S (S n)[//]nexp_resp_ap_zero (S (S n)) H14). astepr (OneR[*][1][/] ([0][+][1][+][1])[*]([0][+][1][+][1])[^]S n[//] mult_resp_ap_zero IR ([0][+][1][+][1]) (([0][+][1][+][1])[^]S n) H14 (nexp_resp_ap_zero (S n) H14)). astepr ([1][*][1][/] ([0][+][1][+][1])[^]S (S n)[//] nexp_resp_ap_zero (S (S n)) H14). rational. astepr (([1][/] [0][+][1][+][1][//]H14)[*]Two[*] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)). astepr (([1][/] [0][+][1][+][1][//]H14)[*]([0][+][1][+][1])[*] nexp IR (S (S n)) ([1][/] [0][+][1][+][1][//]H14)). apply mult_wdr. 3: apply plus_resp_less_both. 3: exact H12. 3: exact H13. astepr (([1][/] [0][+][1][+][1][//]H14)[^]S (S n)). apply eq_symmetric_unfolded. apply nexp_distr_recip. astepl ([1][+][1][/] ([0][+][1][+][1])[^]S (S n)[//] nexp_resp_ap_zero (S (S n)) H14). 2: rational. astepl ([0][+][1][+][1][/] ([0][+][1][+][1])[^]S (S n)[//] nexp_resp_ap_zero (S (S n)) H14). rstepr ([0][+][1][+][1][/] ([0][+][1][+][1])[*]([0][+][1][+][1])[^]S n[//] mult_resp_ap_zero IR ([0][+][1][+][1]) (([0][+][1][+][1])[^]S n) H14 (nexp_resp_ap_zero (S n) H14)). astepl ([0][+][1][+][1][/] ([0][+][1][+][1])[*]([0][+][1][+][1])[^]S n[//] mult_resp_ap_zero IR ([0][+][1][+][1]) (([0][+][1][+][1])[^]S n) H14 (nexp_resp_ap_zero (S n) H14)). apply eq_reflexive_unfolded. Qed.
imports: CoRN.metrics.Prod_Sub CoRN.metrics.Equiv