diamond: min/max and order_dual

Stream: general

[Yury G. Kudryashov]

If I have [decidable_linear_order α], then I have two non-defeq has_sup on order_dual α: @min α _ and @max (order_dual α) _. Most of the time it doesn't matter but sometimes this stops me from using the := @some_lemma (order_dual α) _ _ trick for a proof.

[Kevin Buzzard]

How is max defined on order_dual?

[Yury G. Kudryashov]

If I unfold everything back to α, then I get if a ≤ b then a else b and if b ≤ a then b else a.

[Kevin Buzzard]

D'oh