proposition: Lemma Omega_limit_Limit {sto : StrictOrder lt} (s: nat -> A) (x:A) : Omega_limit s x -> Limit x.
proof: Proof. destruct 1 as [H H0]; split. - exists (s 0); auto. - intros y Hlt; destruct (H0 _ Hlt) as [z Hz]. exists (s z); split; auto. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles Setoid)