Auxiliary definition to define argmax

argmax f l returns some a, where a of l that maximises f a. If there are a b such that f a = f b, it returns whichever of a or b comes first in the list. argmax f [] = none`

argmin f l returns some a, where a of l that minimises f a. If there are a b such that f a = f b, it returns whichever of a or b comes first in the list. argmin f [] = none`

maximum l returns an with_bot α, the largest element of l for nonempty lists, and ⊥ for []

minimum l returns an with_top α, the smallest element of l for nonempty lists, and ⊤ for []