proposition: Lemma Omega_limit_not_Succ {sto : StrictOrder lt} (s: nat -> A) (x:A) : Omega_limit s x -> forall y, ~ Successor x y.
proof: Proof. intros [Hlim Hlim0] y [Hsucc Hsucc0]. destruct (Hlim0 _ Hsucc) as [i Hi]. absurd (lt (s i) (s i)). + apply sto. + destruct (Hsucc0 _ Hi (Hlim i)). Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles Setoid)