```module Orn.AlgebraicOrnament.Examples.Leq where

open import Logic.IProp

open import Data.Unit
open import Data.Nat hiding (_+_ ; fold)
open import Data.Fin hiding (lift ; _+_ ; fold)
open import Data.Product

open import Relation.Binary.PropositionalEquality

open import IDesc.IDesc
open import IDesc.Fixpoint
open import IDesc.InitialAlgebra

open import IDesc.Examples.Nat

import  Orn.AlgebraicOrnament
import  Orn.AlgebraicOrnament.Coherence

-- Paper: Example 4.23

α+m : Nat → Alg NatD (λ _ → Nat)
α+m m {tt} (zero , tt) = m
α+m m {tt} (suc zero , n) = su n
α+m m {tt} (suc (suc ()) , _)

_+_ : Nat → Nat → Nat
m + n = fold NatD (α+m m) n

_≦_ : Nat → Nat → Set
m ≦ n = μ algOrnD (tt , n)
where open Orn.AlgebraicOrnament.Func NatD (α+m m)

ize : ∀{m} → m ≦ m
ize = ⟨ (zero , tt) , refl , tt ⟩

isu : ∀{m n} → m ≦ n → m ≦ su n
isu {m}{n} ik = ⟨ (suc zero , n) , refl , ik ⟩

forgetOrnament : ∀{m n} → m ≦ n → Nat
forgetOrnament {m} = forgetAlgOrn
where open Orn.AlgebraicOrnament.Coherence NatD (α+m m)

lemma-coherence : ∀ {m n} → (t : m ≦ n) → ⊢ n ≡ m + forgetOrnament t
lemma-coherence {m} = coherentOrn
where open Orn.AlgebraicOrnament.Coherence NatD (α+m m)
```