### Browse the appendix:

- Z1 (Zermelo's 1904 proof, implemented by Jonas Kaiser/Danko Ilik)
- Z2 (Zermelo's 1908 proof, implemented by Chad Brown)
- EQ (equality/equivalence of both constructed orderings)

Documentation generated by Coqdoc. Click the respective index.html for an overall index of definitions and lemmas.