{-# OPTIONS --sized-types #-}
module ZilibowitzRubenHenner2 where

open import Size
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product

 
data Nat : {_ : Size} -> Set where
  zero : ∀ {size} → Nat {↑ size} 
  suc  : ∀ {size} → Nat {size} → Nat {↑ size}

{-# BUILTIN NATURAL Nat  #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

{-
data _≤_ : -- ∀ {size} →
           Rel (Nat {∞}) where
  z≤n : ∀ {n}                 → zero ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
-}

data _≤_ : Rel (Nat {∞}) where
  z≤n : ∀ {sm sn}                {n : Nat {sn}}               → zero {sm} ≤ n
  s≤s : ∀ {sm sn} {m : Nat {sm}} {n : Nat {sn}} (m≤n : m ≤ n) → suc {sm} m ≤ suc {sn} n


≤-refl : (n : Nat {∞}) → n ≤ n
≤-refl zero    = z≤n 
≤-refl (suc n) = s≤s (≤-refl n)

_<_ : ∀ {size} → Nat {size} → Nat → Set
_<_ {size} m n = suc {size} m ≤ n

z : ∀ {size} → (n : Nat {↑ size}) → (zero {size} < n) → ∃ {Nat {size}} (λ m → m < n)
z zero ()
z (suc n) _ = n , (≤-refl (suc n))

j : ∀ {size} → Nat {size} -> Nat
j zero = zero
j (suc n) = helper (suc n) (z (suc n) (s≤s z≤n))
 where
 helper : {size : Size} -> (sn : Nat {↑ size}) -> ∃ {Nat {size}} (λ n → n < sn) -> Nat
 helper sn (n , _) = j n