Closed stefan-aws closed 1 year ago
Establishes that every totally-ordered set has a unique minimum.
The proof is a simplified version of the arguments in https://leino.science/papers/krml275.html.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.
Establishes that every totally-ordered set has a unique minimum.
The proof is a simplified version of the arguments in https://leino.science/papers/krml275.html.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.