Minimal elements of finite posets

Auxiliary lemmas used by the rollback development: every nonempty finite subset of a partial order with well-founded strict order (or, constructively, of any partial order) has a minimal element.

theorem EventStructures.Finset.exists_minimal_of_nonempty {α : Type u_1} [PartialOrder α] [WellFoundedLT α] (T : Finset α) (hne : T.Nonempty) : ∃ x ∈ T, ∀ y ∈ T, y < x → False

Classical: A non-empty finite subset of a well-founded partial order has a minimal element.

theorem EventStructures.Finset.exists_minimal_dec {α : Type u_1} [PartialOrder α] (T : Finset α) (hne : T.Nonempty) : ∃ x ∈ T, ∀ y ∈ T, ¬y < x

Constructive: every nonempty finite subset of a decidable strict order has a minimal element (no well-foundedness needed).