Source code on Github
-- {-# OPTIONS --safe #-}
open import Prelude.Init; open SetAsType
open import Prelude.Decidable
open import Prelude.DecEq.Core
open import Prelude.Lists
open import Prelude.InferenceRules

open import Prelude.Ord.Core
open import Prelude.Ord.Dec

module Prelude.Ord.MinMax {A : Type }  _ : Ord A   _ : DecOrd A  where

min max : Op₂ A
min x y = if  x ≤? y  then x else y
max x y = if  y ≤? x  then x else y

minimum maximum : A  List A  A
minimum = foldl min
maximum = foldl max

minimum⁺ maximum⁺ : List⁺ A  A
minimum⁺ (x  xs) = minimum x xs
maximum⁺ (x  xs) = maximum x xs

module _ {x} {y} {ys : List A} where

  minimum-skip :
    x  y
    ─────────────────────────────────
    minimum x (y  ys)  minimum x ys
  minimum-skip x≤ rewrite dec-yes (x ≤? y) x≤ .proj₂ = refl

  maximum-skip :
    y  x
    ─────────────────────────────────
    maximum x (y  ys)  maximum x ys
  maximum-skip y≤ rewrite dec-yes (y ≤? x) y≤ .proj₂ = refl

postulate
  ∀≤max⁺ :  (xs : List⁺ A)  All⁺ (_≤ maximum⁺ xs) xs
  ∀≤max :  x (xs : List A)  All (_≤ maximum x xs) xs

∀≤⇒≡max :  {x} {xs : List A} 
  All (_≤ x) xs
  ────────────────
  x  maximum x xs
∀≤⇒≡max [] = refl
∀≤⇒≡max {x = x} {xs = y  xs} (py  p) =
  begin x                  ≡⟨ ∀≤⇒≡max {xs = xs} p 
        maximum x xs       ≡˘⟨ maximum-skip {ys = xs} py 
        maximum x (y  xs)  where open ≡-Reasoning