proposition: Lemma is_lim_seq_spec : forall u l, is_lim_seq' u l <-> is_lim_seq u l.
proof: Proof. destruct l as [l| |] ; split. - intros H P [eps LP]. destruct (H eps) as [N HN]. exists N => n Hn. apply LP. now apply HN. - intros LP eps. specialize (LP (fun y => Rabs (y - l) < eps)). apply LP. now exists eps. - intros H P [M LP]. destruct (H M) as [N HN]. exists N => n Hn. apply LP. now apply HN. - intros LP M. specialize (LP (fun y => M < y)). apply LP. now exists M. - intros H P [M LP]. destruct (H M) as [N HN]. exists N => n Hn. apply LP. now apply HN. - intros LP M. specialize (LP (fun y => y < M)). apply LP. now exists M. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy