Module mathcomp.classical.wochoice

# Well-ordered choice This file provides proofs of Zorn's lemma, Hausdorff maximal principle, and the well-ordering principle. It does not rely on `classical_sets.v`. NB: Some definitions are likely to move to MathComp. Similar definitions can be found in `classical_sets.v` but expressed with `Prop` instead of `bool` (in particular); there is likely to be more sharing in the future. ``` nonempty A := exists x, x \in A {in <= S, P} == the predicate P holds for all subsets of S P has type {pred T} -> Prop for T : predArgType. maximal R z == z is a maximal element for the relation R minimal R z == z is a minimal element for the relation R upper_bound R A z == for all x in A, we have R x z lower_bound R A z == for all x in A, we have R z x preorder R == R is reflexive and transitive partial_order R == R is an antisymmetric preorder total_order R == R is a total partial order minimum_of R A z := z \in A /\ lower_bound A z maximum_of R A z := z \in A /\ upper_bound A z well_order R == every non-empty subset has a unique minimum element chain R C == the subset C is totally ordered := {in C &, total R} wo_chain R C := {in <= C, well_order R} ```