proposition: Lemma Least_not_Limit {sto : StrictOrder lt} x : Least x -> ~ Limit x.
proof: Proof. intros H [[w H0] H1]. specialize (H w). destruct H, (StrictOrder_Irreflexive x); trivial. now transitivity y. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles Setoid)