Min and max for all total orders #1488
Description
Right now we have it for decidable total orders, but given that it merely exists for all total orders, and that the lub/glb is unique, we shouldn't need decidability.
{{ message }}
Right now we have it for decidable total orders, but given that it merely exists for all total orders, and that the lub/glb is unique, we shouldn't need decidability.