proposition: Lemma Least_not_Succ {sto : StrictOrder lt} (x:A) : Least x -> forall z, ~ Successor x z.
proof: Proof. intros H z [H0 H1]; specialize (H z). inversion H; subst. - eapply H1; eauto. now transitivity z. - destruct sto; eauto. Qed.
imports: Coq(RelationClasses Relation_Operators Ensembles Setoid)