{-# OPTIONS --without-K --rewriting #-}

module Pi.Lehmer.Lehmer where

open import lib.Base
open import lib.types.Nat using (_+_)
open import lib.types.Sigma
open import lib.NType
open import lib.PathGroupoid

open import Pi.Common.Arithmetic

data Lehmer : (n : ℕ) -> Type₀ where
  CanZ : Lehmer 0
  CanS : {n : ℕ} -> (l : Lehmer n) -> {r : ℕ} -> (r ≤ S n) -> Lehmer (S n)

-- off-by-one
-- Lehmer 1 has two elements

private
  x y : Lehmer 1
  x = CanS CanZ z≤n -- r = 0
  y = CanS CanZ (s≤s z≤n) -- r = 1