proposition: Lemma MSseqLimit'_imp_MSseqLimit : forall (X : CPsMetricSpace) (seq : nat -> X) (lim : X), MSseqLimit' seq lim -> MSseqLimit seq lim.
proof: Proof. intros X seq lim. unfold MSseqLimit' in |- *. intro H. unfold MSseqLimit in |- *. intros n H0. elim H with (power n 2). intros p H1. exists p. intros m H2. apply leEq_less_trans with (one_div_succ (R:=IR) (power n 2)). apply H1. exact H2. unfold one_div_succ in |- *. astepr (OneR[^]n[/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H0). astepr (OneR[/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H0). apply recip_resp_less. apply nexp_resp_pos. apply pos_two. unfold Snring in |- *. simpl in |- *. apply less_wdr with (nexp IR n Two[+][1]). apply shift_less_plus. astepl (nexp IR n Two[-][1]). apply minusOne_less. astepl (OneR[+]nexp IR n Two). astepr (OneR[+]nring (power n 2)). apply plus_resp_eq. apply nexp_power. Qed.
imports: CoRN.metrics.CPseudoMSpaces