```
module Miscellaneous where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _∸_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
  -- We don't use the library version of ≤-<-connex 
  using (n≤0⇒n≡0; ≤-refl; ≤-trans; <-trans; <-irrefl; <⇒≤; ≤-pred; <-transˡ; m≤n⇒m<n∨m≡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.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_)
open import Function using (_∘_; id)
open import Data.Maybe using (Maybe; just; nothing)
```

Some basic stuff
```
just≢nothing : {A : Set} {x : A} → just x ≢ nothing
just≢nothing ()

infixr  _⇔_
_⇔_ : Set → Set → Set
A ⇔ B = (A → B) × (B → A)

NonEmpty : {A : Set} → (A → Set) → Set
-- NonEmpty P = ∃[ x ] P x
NonEmpty S = ∃[ x ] x ∈ S

-- image of S under f
_[_] : {A B : Set} → (A → B) → (A → Set) → B → Set
f [ S ] = λ y → ∃[ x ] (x ∈ S × f x ≡ y)

module _ {A B : Set} (f : A → B) (S : A → Set) where
  member-image : {x : A} → x ∈ S → f x ∈ f [ S ]
  member-image {x} x∈S = x , x∈S , refl

  nonempty-image : NonEmpty S → NonEmpty (f [ S ])
  nonempty-image (x , x∈S) = f x , member-image x∈S
```

Some lemmas I couldn't find in the standard library:
```
≤-suc : {m n : ℕ} → m ≤ suc n → (m ≤ n ⊎ m ≡ suc n)
≤-suc {zero} {n} _ = inj₁ z≤n
≤-suc {suc m} {zero} (s≤s h) = inj₂ (cong suc (n≤0⇒n≡0 h))
≤-suc {suc m} {suc n} (s≤s h) with ≤-suc {m} {n} h
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ m≡1+n = inj₂ (cong suc m≡1+n)

n<⇒suc : {n m : ℕ} → n < m → ∃ (λ k → m ≡ suc k)
n<⇒suc {n} {suc m} (s≤s n<m) = m , refl
```

We define ≤-<-connex differently from stdlib.
```
≤-<-connex : (m n : ℕ) → m ≤ n ⊎ n < m
≤-<-connex zero n = inj₁ z≤n
≤-<-connex (suc m) zero = inj₂ (s≤s z≤n)
≤-<-connex (suc m) (suc n) with ≤-<-connex m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n<m = inj₂ (s≤s n<m)

≤-<-connex-≤ : (m n : ℕ) → (m≤n : m ≤ n) → ≤-<-connex m n ≡ inj₁ m≤n
≤-<-connex-≤ zero n z≤n = refl
≤-<-connex-≤ (suc m) (suc n) (s≤s m≤n) rewrite ≤-<-connex-≤ m n m≤n = refl

≤-<-connex-> : (m n : ℕ) → (n<m : n < m) → ≤-<-connex m n ≡ inj₂ n<m
≤-<-connex-> (suc m) zero (s≤s z≤n) = refl
≤-<-connex-> (suc m) (suc n) (s≤s n<m) rewrite ≤-<-connex-> m n n<m = refl

1+n∸n≡1 : (n : ℕ) → suc n ∸ n ≡ 
1+n∸n≡1 zero = refl
1+n∸n≡1 (suc n) = 1+n∸n≡1 n

case₃-⊎ : {A B C D : Set} → (A → D) → (B → D) → (C → D) → (A ⊎ B ⊎ C) → D
case₃-⊎ f g h = case-⊎ f (case-⊎ g h)

i<j-cmp : (i j n : ℕ) → i < j → ((i ≤ n × j ≤ n) ⊎ (i ≤ n × n < j) ⊎ (n < i × n < j))
i<j-cmp i j n i<j = case-⊎ (λ j≤n → inj₁ ((<⇒≤ (<-transˡ i<j j≤n)) , j≤n)) 
                           (λ n<j → case-⊎ (λ i≤n → inj₂ (inj₁ (i≤n , n<j))) 
                                           (λ n<i → inj₂ (inj₂ (n<i , n<j))) 
                                           (≤-<-connex i n))
                           (≤-<-connex j n)
```

Switching from one function to another at n.
```
module _ {A : Set} (f g : ℕ → A) where
  switch : ℕ → ℕ → A
  switch n x = case-⊎ (λ n≤x → g x) (λ x<n → f x) (≤-<-connex n x)

  switch-< : (n x : ℕ) → x < n → switch n x ≡ f x
  switch-< n x x<n rewrite ≤-<-connex-> n x x<n = refl

  switch-≥ : (n x : ℕ) → n ≤ x → switch n x ≡ g x
  switch-≥ n x x≥n rewrite ≤-<-connex-≤ n x x≥n = refl
```

Switching from one function to another at n + 1.
```
  switch′ : ℕ → ℕ → A
  switch′ n x = case-⊎ (λ x≤n → f x) (λ n<x → g x) (≤-<-connex x n)

  switch′-≤ : (n x : ℕ) → x ≤ n → switch′ n x ≡ f x
  switch′-≤ n x x≤n rewrite ≤-<-connex-≤ x n x≤n = refl

  switch′-> : (n x : ℕ) → n < x → switch′ n x ≡ g x
  switch′-> n x n<x rewrite ≤-<-connex-> x n n<x = refl
```

Disjunctive syllogism
```
⊎-¬ˡ : {A B : Set} → A ⊎ B → ¬ A → B
⊎-¬ˡ (inj₁ x) h = ⊥-elim (h x)
⊎-¬ˡ (inj₂ y) h = y

⊎-¬ʳ : {A B : Set} → A ⊎ B → ¬ B → A
⊎-¬ʳ (inj₁ x) h = x
⊎-¬ʳ (inj₂ y) h = ⊥-elim (h y)
```

Intuitionistic validties concerning quantifiers
```
¬∃⟶∀¬ : {A : Set} {B : A → Set} → ¬ (Σ[ x ∈ A ] B x) → ∀ (x : A) → ¬ B x
¬∃⟶∀¬ ¬∃ x Bx = ¬∃ (x , Bx)
```

```
Increasing : {A : Set} → (A → A → Set) → (ℕ → A) → Set
Increasing _≼_ f = (m n : ℕ) → m < n → f m ≼ f n

increasing-≤ : (f : ℕ → ℕ) → Increasing _<_ f → (m n : ℕ) → m ≤ n → f m ≤ f n
increasing-≤ f h m n m≤n = case-⊎ (λ m<n → <⇒≤ (h m n m<n)) 
                                  (λ {refl → ≤-refl})
                                  (m≤n⇒m<n∨m≡n m≤n)

increasing-step-increasing : (f : ℕ → ℕ) → ((n : ℕ) → f n < f (suc n)) → Increasing _<_ f
increasing-step-increasing f f-step m (suc n) m<1+n with ≤-suc m<1+n
... | inj₁ m<n = <-trans (increasing-step-increasing f f-step m n m<n) (f-step n)
... | inj₂ refl = f-step m

subseq-increasing : {A : Set} (_≼_ : A → A → Set) (f : ℕ → A) (r : ℕ → ℕ) 
  → Increasing _≼_ f
  → Increasing _<_ r
  ------------------------
  → Increasing _≼_ (f ∘ r)
subseq-increasing _≼_ f r f-increasing r-increasing m n m<n
  = f-increasing (r m) (r n) (r-increasing m n m<n)

id-increasing : Increasing _<_ id
id-increasing m n m<n = m<n

AgreeUpTo : {A : Set} → ℕ → (ℕ → A) → (ℕ → A) → Set
AgreeUpTo n f g = {m : ℕ} → m ≤ n → f m ≡ g m

agreeUpTo-≤ : {A : Set} {n m : ℕ} {f g : ℕ → A}
  → AgreeUpTo n f g
  → m ≤ n
  -----------------
  → AgreeUpTo m f g
agreeUpTo-≤ h m≤n x≤m = h (≤-trans x≤m m≤n)

agreeUpTo-reflexive : {A : Set} (n : ℕ) (f : ℕ → A) → AgreeUpTo n f f
agreeUpTo-reflexive n f _ = refl

agreeUpTo-symmetric : {A : Set} (n : ℕ) (f g : ℕ → A) → AgreeUpTo n f g → AgreeUpTo n g f
agreeUpTo-symmetric n f g h x≤n = sym (h x≤n)

agreeUpTo-transitive : {A : Set} {n : ℕ} {f : ℕ → A} {g : ℕ → A} {k : ℕ → A}
  → AgreeUpTo n f g
  → AgreeUpTo n g k
  -----------------
  → AgreeUpTo n f k
agreeUpTo-transitive hfg hgk m≤n = trans (hfg m≤n) (hgk m≤n)

InitialSegmentProperty : {A : Set} (P : (ℕ → A) → Set) → Set
InitialSegmentProperty {A} P = (f : ℕ → A) → ((n : ℕ) → ∃[ g ] (g ∈ P × AgreeUpTo n f g)) → f ∈ P

ISP-closed-∩ : {A : Set} (P Q : (ℕ → A) → Set)
  → InitialSegmentProperty P
  → InitialSegmentProperty Q
  ------------------------------------------
  → InitialSegmentProperty (λ f → f ∈ P × f ∈ Q)
ISP-closed-∩ P Q P-isp Q-isp f h = 
  P-isp f (λ n → proj₁ (h n) , proj₁ (proj₁ (proj₂ (h n))) , proj₂ (proj₂ (h n))) , 
  Q-isp f (λ n →  proj₁ (h n) , proj₂ (proj₁ (proj₂ (h n))) , proj₂ (proj₂ (h n)))
```