order_dual disappointment

Stream: maths

[Chris Hughes]

How sad...

example (a b : β) : max a b = @min (order_dual β) _ a b := rfl --doesn't work

[Kenny Lau]

import order.basic
variables (β : Type*) [decidable_linear_order β]
example (a b : β) : max a b = @min (order_dual β) _ b a := rfl --works

[Chris Hughes]

I might go and change the definition of list.maximum, with this in mind, and swap the order