# Imports

```
module Functions.Universal_Quantification where

open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; _<_; z≤n; s≤s; _≤′_; ≤′-step; ≤′-refl)
open import Data.Fin using (Fin; zero; suc; toℕ)
open import Data.Empty using (⊥)
open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function using (flip; _\$_; _∘_)```

# Universal quantification

We can represent a proof for universal quantification on a set by a dependent function on that set. For example:

```
≤-refl : (n : ℕ) → n ≤ n
≤-refl zero    = z≤n
≤-refl (suc n) = s≤s (≤-refl n)```

## Exercises

Define the following functions (that is, prove those properties):

```
≤-trans : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
total   : ∀ m n → m ≤ n ⊎ n ≤ m
≤-pred  : ∀ {m n} → suc m ≤ suc n → m ≤ n
≤-mono  : ∀ {m n k} → n ≤ m → k + n ≤ k + m```

Hint: For `total`, use the previously defined `[_,_]` function.

Note that, from the properties above, it follows that `_≤_` is a total order on `ℕ`. (We can take `_≤_` as a relation over `ℕ`.)

## Exercises

Define the following functions:

```
≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤′⇒≤   : ∀ {a b} → a ≤′ b → a ≤ b
z≤′n   : ∀ n → zero ≤′ n
s≤′s   : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
≤⇒≤′   : ∀ {a b} → a ≤ b → a ≤′ b
fin≤   : ∀ {n}(m : Fin n) → toℕ m < n```