fact: Record well_ordered X := { wo_total: ∀ x y, x ∈ X → y ∈ X → x ≼ y ∨ y ≼ x; wo_minima: ∀ Y, Y ⊆ X → inhabited Y → ∃ m, m ∈ Y ∧ ∀ x, x ∈ Y → m ≼ x }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)