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 |- *. intro n. set (H2 := two_ap_zero IR) in *. elim H with (S n) H2. intros p H3. exists p. intros m H4. apply less_leEq. apply less_transitive_unfolded with ((OneR[/] Two:IR[//]H2)[^]S n). apply H3. exact H4. unfold one_div_succ in |- *. unfold Snring in |- *. astepl (OneR[^]S n[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H2). astepl (OneR[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H2). apply bin_less_un. Qed.
imports: CoRN.metrics.CPseudoMSpaces