{-
  Dickson's Lemma (simple version).
    Every function f : ℕ → ℕ is good in the sense that
    there exists i ∈ ℕ such that f(i) ≤ f(i+1).

  Proof (classical).
    Any such function f somewhere attains a global minimum f(i).
    This minimum satisfies f(i) ≤ f(j) for all j ∈ ℕ.
    In particular, f(i) ≤ f(i+1).

  Nice and efficient proof!
  But: This proof does not give a clue how to find a suitable index i. :-(
-}

module Antwerp.Dickson where

open import Data.Nat
open import Data.Product

-- For any function "f", "Good f" is the type of
-- witnesses that "f" is good.
Good : (ℕ → ℕ) → Set
Good f = Σ[ i ∈ ℕ ] f i ≤ f (suc i)

example : ℕ → ℕ
example  = 
example  = 
example  = 
example _ = 

module Classical where
  open import Antwerp.Minimum.Classical

  theorem : (f : ℕ → ℕ) → Good f
  theorem f with minimum f
  ... | i , p = i , p (suc i)

module ConstructiveButUninformative (⊥ : Set) where
  open import Antwerp.Minimum.Constructive ⊥

  theorem : (f : ℕ → ℕ) → ¬ ¬ (Good f)
  theorem f = do
    i , p ← minimum f
    q     ← p (suc i)
    return (i , q)

module Constructive where
  theorem : (f : ℕ → ℕ) → Good f
  theorem f = ConstructiveButUninformative.theorem (Good f) f λ r → r