Some stuff that depends on the ecluded middle.

```
module Classical where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst)
open import Data.Nat using (; zero; suc; _≤_; s≤s; z≤n; _<_)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_)
open import Data.Empty using (; ⊥-elim)
open import Relation.Unary using (_∈_)
open import Function using (_∘_; id)

open import Miscellaneous
```

The excluded middle and some consequences
```
postulate
  em : {A : Set}  A  ¬ A

¬¬-elim : {A : Set}  ¬ ¬ A  A
¬¬-elim {A} h with em {A}
... | inj₁ x = x
... | inj₂ y = ⊥-elim (h y)

¬∀⟶∃¬ : {A : Set} {B : A  Set}  ¬ (∀ (x : A)  B x)  Σ[ x  A ] ¬ (B x)
¬∀⟶∃¬ {A} {B} ¬∀xBx = ¬¬-elim  ¬∃x¬Bx  ¬∀xBx  x  ¬¬-elim  ¬Bx  ¬∃x¬Bx (x , ¬Bx))))

¬∀∃⟶∃∀¬ : {A : Set} {B : A  Set} {C : (x : A)  B x  Set}
   ¬ (∀ (x : A)  Σ[ y  B x ] C x y)
  ------------------------------------
   Σ[ x  A ]  (y : B x)  ¬ C x y
¬∀∃⟶∃∀¬ ¬∀∃ with ¬∀⟶∃¬ ¬∀∃ 
... | x , ¬∃ = x , (¬∃⟶∀¬    ¬∃ ))

infinite-or-cofinite-¬ : (P :   Set)
   ((k : )  Σ[ l   ] k < l × P l)  Σ[ k   ] ((l : )  k < l  ¬ P l)
infinite-or-cofinite-¬ P = case-⊎ inj₁  z  inj₂ (h z)) (em {A = (k : )  Σ[ l   ] k < l × P l})
  where
  h : ¬ ((k : )  Σ[ l   ] k < l × P l)  Σ[ k   ] ((l : )  k < l  ¬ P l)
  h ¬inf = k , λ l k<l z  h₂ (l , k<l , z)
    where
    h₁ : Σ[ k   ] ¬ (Σ[ l   ] k < l × P l)
    h₁ = ¬∀⟶∃¬ ¬inf
    k : 
    k = proj₁ h₁
    h₂ : ¬ (Σ[ l   ] k < l × P l)
    h₂ = proj₂ h₁
```

The least number principle requires decidability of A.
```
leastNumber-aux : {A :   Set} (x : )
   A x
  --------------------------------------------
   Σ[ z   ] (A z × ((y : )  A y  z  y))
leastNumber-aux {A} x Ax with x | em {A zero}
... | _     | inj₁ A0  = zero , A0 , λ y _  z≤n
... | zero  | inj₂ ¬A0 = ⊥-elim (¬A0 Ax)
... | suc x | inj₂ ¬A0 = 
    suc z , A1+z , 
     {zero A0        ⊥-elim (¬A0 A0)
       ; (suc y) A1+y  s≤s (h′ y A1+y)
       })
  where
  h : Σ[ z   ] A (suc z) × ((y : )  A (suc y)  z  y)
  h = leastNumber-aux {A  suc} x Ax
  z = proj₁ h
  A1+z = proj₁ (proj₂ h)
  h′ : (y : )  A (suc y)  z  y
  h′ = proj₂ (proj₂ h)

leastNumberPrinciple : {A :   Set}  NonEmpty A  Σ[ z   ] (z  A × ((y : )  y  A  z  y))
leastNumberPrinciple (x , Ax) = leastNumber-aux x Ax

leastSeqAt : {S : (  )  Set}
   NonEmpty S
   (n : )
  --------------------------------------------------------------
   Σ[ f  (  ) ] (f  S × ((g :   )  g  S  f n  g n))
leastSeqAt {S} S-nonempty n = f , f∈S , f-minimal
  where
  A :   Set
  -- A x = Σ[ g ∈ (ℕ → ℕ) ] (S g × g n ≡ x)
  A =  g  g n) [ S ]
  A-nonempty : NonEmpty A
  A-nonempty = nonempty-image  g  g n) S S-nonempty
  min-A : Σ[ z   ] (z  A × ((w : )  w  A  z  w))
  min-A = leastNumberPrinciple A-nonempty
  z : 
  z = proj₁ min-A
  z∈A : z  A
  z∈A = proj₁ (proj₂ min-A)
  z-minimal : (w : )  w  A  z  w
  z-minimal = proj₂ (proj₂ min-A)
  f :   
  f = proj₁ z∈A
  f∈S : f  S
  f∈S = proj₁ (proj₂ z∈A)
  fn≡z : f n  z
  fn≡z = proj₂ (proj₂ z∈A)
  f-minimal : (g :   )  g  S  f n  g n
  -- f-minimal g g∈S = subst (_≤ g n) (sym fn≡z) (z-minimal (g n) (member-image (λ g → g n) S g∈S))
  f-minimal g g∈S rewrite fn≡z = z-minimal (g n) (member-image  g  g n) S g∈S)
```