Strictly Monotone Brouwer Trees

This is a Coq version of the theory described in the paper Strictly Monotone Brouwer Trees for Well-founded Recursion Over Multiple Arguments by Joseph Eremondi.

The library offers a constructive definition of Brouwer trees, an intuitionistic variant of ordinals.

The type of ordinals is equipped with three construction operations: zero, succ, lim. It is also equipped with a preorder ≤, which induces an equivalence ≡. The corresponding strict preorder < is well-founded.

Ordinals also support a binary least upper bound function, max, which is strictly monotone: that is, t < t' and u < u' imply max t u < max t' u'.