    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Natural numbers, basic types and operations
    ------------------------------------------------------------------------

    -- See README.Data.Nat for examples of how to use and reason about
    -- naturals.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Nat.Base where

    open import Algebra.Bundles.Raw using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring)
    open import Algebra.Definitions.RawMagma using (_∣ˡ_; _,_)
    open import Data.Bool.Base using (Bool; true; false; T; not)
    open import Data.Parity.Base using (Parity; 0ℙ; 1ℙ)
    open import Level using (0ℓ)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.PropositionalEquality.Core
      using (_≡_; _≢_; refl; cong)
    open import Relation.Nullary.Negation.Core using (¬_; contradiction)
    open import Relation.Unary using (Pred)

    ------------------------------------------------------------------------
    -- Types

    open import Agda.Builtin.Nat public
      using (zero; suc) renaming (Nat to ℕ)

    --smart constructor
    pattern 2+ n = suc (suc n)

    ------------------------------------------------------------------------
    -- Boolean equality relation

    open import Agda.Builtin.Nat public
      using () renaming (_==_ to _≡ᵇ_)

    ------------------------------------------------------------------------
    -- Boolean ordering relation

    open import Agda.Builtin.Nat public
      using () renaming (_<_ to _<ᵇ_)

    infix 4 _≤ᵇ_
    _≤ᵇ_ : (m n : ℕ) → Bool
    zero  ≤ᵇ n = true
    suc m ≤ᵇ n = m <ᵇ n

    ------------------------------------------------------------------------
    -- Standard ordering relations

    infix 4 _≤_ _<_ _≥_ _>_ _≰_ _≮_ _≱_ _≯_

    data _≤_ : Rel ℕ 0ℓ where
      z≤n : ∀ {n}                 → zero  ≤ n
      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

    _<_ : Rel ℕ 0ℓ
    m < n = suc m ≤ n

    -- Smart constructors of _<_

    pattern z<s     {n}     = s≤s (z≤n {n})
    pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
    pattern sz<ss   {n}     = s<s (z<s {n})

    -- Smart destructors of _≤_, _<_

    s≤s⁻¹ : ∀ {m n} → suc m ≤ suc n → m ≤ n
    s≤s⁻¹ (s≤s m≤n) = m≤n

    s<s⁻¹ : ∀ {m n} → suc m < suc n → m < n
    s<s⁻¹ (s<s m<n) = m<n

    ------------------------------------------------------------------------
    -- Other derived ordering relations

    _≥_ : Rel ℕ 0ℓ
    m ≥ n = n ≤ m

    _>_ : Rel ℕ 0ℓ
    m > n = n < m

    _≰_ : Rel ℕ 0ℓ
    a ≰ b = ¬ a ≤ b

    _≮_ : Rel ℕ 0ℓ
    a ≮ b = ¬ a < b

    _≱_ : Rel ℕ 0ℓ
    a ≱ b = ¬ a ≥ b

    _≯_ : Rel ℕ 0ℓ
    a ≯ b = ¬ a > b

    ------------------------------------------------------------------------
    -- Simple predicates

    -- Defining these predicates in terms of `T` and therefore ultimately
    -- `⊤` and `⊥` allows Agda to automatically infer them for any natural
    -- of the correct form. Consequently in many circumstances this
    -- eliminates the need to explicitly pass a proof when the predicate
    -- argument is either an implicit or an instance argument. See `_/_`
    -- and `_%_` further down this file for examples.
    --
    -- Furthermore, defining these predicates as single-field records
    -- (rather defining them directly as the type of their field) is
    -- necessary as the current version of Agda is far better at
    -- reconstructing meta-variable values for the record parameters.

    -- A predicate saying that a number is not equal to 0.

    record NonZero (n : ℕ) : Set where
      field
        nonZero : T (not (n ≡ᵇ 0))

    -- Instances

    instance
      nonZero : ∀ {n} → NonZero (suc n)
      nonZero = _

    -- Constructors

    ≢-nonZero : ∀ {n} → n ≢ 0 → NonZero n
    ≢-nonZero {zero}  0≢0 = contradiction refl 0≢0
    ≢-nonZero {suc n} n≢0 = _

    >-nonZero : ∀ {n} → n > 0 → NonZero n
    >-nonZero z<s = _

    -- Destructors

    ≢-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n ≢ 0
    ≢-nonZero⁻¹ (suc n) ()

    >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
    >-nonZero⁻¹ (suc n) = z<s

    -- The property of being a non-zero, non-unit

    record NonTrivial (n : ℕ) : Set where
      field
        nonTrivial : T (1 <ᵇ n)

    -- Instances

    instance
      nonTrivial : ∀ {n} → NonTrivial (2+ n)
      nonTrivial = _

    -- Constructors

    n>1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n
    n>1⇒nonTrivial sz<ss = _

    -- Destructors

    nonTrivial⇒nonZero : ∀ n → .{{NonTrivial n}} → NonZero n
    nonTrivial⇒nonZero (2+ _) = _

    nonTrivial⇒n>1 : ∀ n → .{{NonTrivial n}} → n > 1
    nonTrivial⇒n>1 (2+ _) = sz<ss

    nonTrivial⇒≢1 : ∀ {n} → .{{NonTrivial n}} → n ≢ 1
    nonTrivial⇒≢1 {{()}} refl

    ------------------------------------------------------------------------
    -- Raw bundles

    open import Agda.Builtin.Nat public
      using (_+_; _*_) renaming (_-_ to _∸_)

    +-rawMagma : RawMagma 0ℓ 0ℓ
    +-rawMagma = record
      { _≈_ = _≡_
      ; _∙_ = _+_
      }

    +-0-rawMonoid : RawMonoid 0ℓ 0ℓ
    +-0-rawMonoid = record
      { _≈_ = _≡_
      ; _∙_ = _+_
      ; ε   = 0
      }

    *-rawMagma : RawMagma 0ℓ 0ℓ
    *-rawMagma = record
      { _≈_ = _≡_
      ; _∙_ = _*_
      }

    *-1-rawMonoid : RawMonoid 0ℓ 0ℓ
    *-1-rawMonoid = record
      { _≈_ = _≡_
      ; _∙_ = _*_
      ; ε = 1
      }

    +-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
    +-*-rawNearSemiring = record
      { Carrier = _
      ; _≈_ = _≡_
      ; _+_ = _+_
      ; _*_ = _*_
      ; 0# = 0
      }

    +-*-rawSemiring : RawSemiring 0ℓ 0ℓ
    +-*-rawSemiring = record
      { Carrier = _
      ; _≈_ = _≡_
      ; _+_ = _+_
      ; _*_ = _*_
      ; 0# = 0
      ; 1# = 1
      }

    ------------------------------------------------------------------------
    -- Arithmetic

    open import Agda.Builtin.Nat
      using (div-helper; mod-helper)

    pred : ℕ → ℕ
    pred n = n ∸ 1

    infix  8 _!
    infixl 7 _⊓_ _⊓′_ _/_ _%_
    infixl 6 _+⋎_ _⊔_ _⊔′_

    -- Argument-swapping addition. Used by Data.Vec._⋎_.

    _+⋎_ : ℕ → ℕ → ℕ
    zero  +⋎ n = n
    suc m +⋎ n = suc (n +⋎ m)

    -- Max.

    _⊔_ : ℕ → ℕ → ℕ
    zero  ⊔ n     = n
    suc m ⊔ zero  = suc m
    suc m ⊔ suc n = suc (m ⊔ n)

    -- Max defined in terms of primitive operations.
    -- This is much faster than `_⊔_` but harder to reason about. For proofs
    -- involving this function, convert it to `_⊔_` with `Data.Nat.Properties.⊔≡⊔‵`.
    _⊔′_ : ℕ → ℕ → ℕ
    m ⊔′ n with m <ᵇ n
    ... | false = m
    ... | true  = n

    -- Min.

    _⊓_ : ℕ → ℕ → ℕ
    zero  ⊓ n     = zero
    suc m ⊓ zero  = zero
    suc m ⊓ suc n = suc (m ⊓ n)

    -- Min defined in terms of primitive operations.
    -- This is much faster than `_⊓_` but harder to reason about. For proofs
    -- involving this function, convert it to `_⊓_` wtih `Data.Nat.properties.⊓≡⊓′`.
    _⊓′_ : ℕ → ℕ → ℕ
    m ⊓′ n with m <ᵇ n
    ... | false = n
    ... | true  = m

    -- Parity

    parity : ℕ → Parity
    parity 0             = 0ℙ
    parity 1             = 1ℙ
    parity (suc (suc n)) = parity n

    -- Division by 2, rounded downwards.

    ⌊_/2⌋ : ℕ → ℕ
    ⌊ 0 /2⌋           = 0
    ⌊ 1 /2⌋           = 0
    ⌊ suc (suc n) /2⌋ = suc ⌊ n /2⌋

    -- Division by 2, rounded upwards.

    ⌈_/2⌉ : ℕ → ℕ
    ⌈ n /2⌉ = ⌊ suc n /2⌋

    -- Naïve exponentiation

    infixr 8 _^_

    _^_ : ℕ → ℕ → ℕ
    x ^ zero  = 1
    x ^ suc n = x * x ^ n

    -- Distance

    ∣_-_∣ : ℕ → ℕ → ℕ
    ∣ zero  - y     ∣ = y
    ∣ x     - zero  ∣ = x
    ∣ suc x - suc y ∣ = ∣ x - y ∣

    -- Distance in terms of primitive operations.
    -- This is much faster than `∣_-_∣` but harder to reason about.
    -- For proofs involving this function, convert it to `∣_-_∣` with
    -- `Data.Nat.Properties.∣-∣≡∣-∣′`.
    ∣_-_∣′ : ℕ → ℕ → ℕ
    ∣ x - y ∣′ with x <ᵇ y
    ... | false = x ∸ y
    ... | true  = y ∸ x

    -- Division
    -- Note properties of these are in `Nat.DivMod` not `Nat.Properties`

    _/_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
    m / (suc n) = div-helper 0 n m n

    -- Remainder/modulus
    -- Note properties of these are in `Nat.DivMod` not `Nat.Properties`

    _%_ : (dividend divisor : ℕ) .{{_ : NonZero divisor}} → ℕ
    m % (suc n) = mod-helper 0 n m n

    -- Factorial

    _! : ℕ → ℕ
    zero  ! = 1
    suc n ! = suc n * n !

    ------------------------------------------------------------------------
    -- Extensionally equivalent alternative definitions of _≤_/_<_ etc.

    -- _≤′_: this definition is more suitable for well-founded induction
    -- (see Data.Nat.Induction)

    infix 4 _≤′_ _<′_ _≥′_ _>′_

    data _≤′_ (m : ℕ) : ℕ → Set where
      ≤′-reflexive : ∀ {n} → m ≡ n → m ≤′ n
      ≤′-step : ∀ {n} → m ≤′ n → m ≤′ suc n

    pattern ≤′-refl {m} = ≤′-reflexive {n = m} refl

    _<′_ : Rel ℕ 0ℓ
    m <′ n = suc m ≤′ n

    -- Smart constructors of _<′_

    pattern <′-base          = ≤′-refl
    pattern <′-step {n} m<′n = ≤′-step {n} m<′n

    _≥′_ : Rel ℕ 0ℓ
    m ≥′ n = n ≤′ m

    _>′_ : Rel ℕ 0ℓ
    m >′ n = n <′ m

    -- _≤″_: this definition of _≤_ is used for proof-irrelevant ‵DivMod`
    -- and is a specialised instance of a general algebraic construction

    infix 4 _≤″_ _<″_ _≥″_ _>″_

    _≤″_ : (m n : ℕ)  → Set
    _≤″_ = _∣ˡ_ +-rawMagma

    _<″_ : Rel ℕ 0ℓ
    m <″ n = suc m ≤″ n

    _≥″_ : Rel ℕ 0ℓ
    m ≥″ n = n ≤″ m

    _>″_ : Rel ℕ 0ℓ
    m >″ n = n <″ m

    -- Smart destructor of _<″_

    s<″s⁻¹ : ∀ {m n} → suc m <″ suc n → m <″ n
    s<″s⁻¹ (k , eq) = k , cong pred eq

    -- _≤‴_: this definition is useful for induction with an upper bound.

    infix 4 _≤‴_ _<‴_ _≥‴_ _>‴_

    data _≤‴_ (m n : ℕ) : Set

    _<‴_ : Rel ℕ 0ℓ
    m <‴ n = suc m ≤‴ n

    data _≤‴_ m n where
      ≤‴-reflexive : m ≡ n → m ≤‴ n
      ≤‴-step      : m <‴ n → m ≤‴ n

    pattern ≤‴-refl = ≤‴-reflexive refl

    _≥‴_ : Rel ℕ 0ℓ
    m ≥‴ n = n ≤‴ m

    _>‴_ : Rel ℕ 0ℓ
    m >‴ n = n <‴ m

    ------------------------------------------------------------------------
    -- A comparison view. Taken from "View from the left"
    -- (McBride/McKinna); details may differ.

    data Ordering : Rel ℕ 0ℓ where
      less    : ∀ m k → Ordering m (suc (m + k))
      equal   : ∀ m   → Ordering m m
      greater : ∀ m k → Ordering (suc (m + k)) m

    compare : ∀ m n → Ordering m n
    compare zero    zero    = equal   zero
    compare (suc m) zero    = greater zero m
    compare zero    (suc n) = less    zero n
    compare (suc m) (suc n) with compare m n
    ... | less    m k = less (suc m) k
    ... | equal   m   = equal (suc m)
    ... | greater n k = greater (suc n) k

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version 2.1

    -- Smart constructors of _≤″_ and _<″_
    pattern less-than-or-equal {k} eq = k , eq
    {-# WARNING_ON_USAGE less-than-or-equal
    "Warning: less-than-or-equal was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.Definitions.RawMagma._∣ˡ_._,_ instead. "
    #-}
    pattern ≤″-offset k = k , refl
    {-# WARNING_ON_USAGE ≤″-offset
    "Warning: ≤″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.Definitions.RawMagma._∣ˡ_ instead. "
    #-}
    pattern <″-offset k = k , refl
    {-# WARNING_ON_USAGE <″-offset
    "Warning: <″-offset was deprecated in v2.1. Please match directly on proofs of ≤″ using pattern (_, refl) from Algebra.Definitions.RawMagma._∣ˡ_ instead. "
    #-}

    -- Smart destructor of _≤″_

    s≤″s⁻¹ : ∀ {m n} → suc m ≤″ suc n → m ≤″ n
    s≤″s⁻¹ (k , eq) = k , cong pred eq
    {-# WARNING_ON_USAGE s≤″s⁻¹
    "Warning: s≤″s⁻¹ was deprecated in v2.1. Please match directly on proofs of ≤″ using constructor Algebra.Definitions.RawMagma._∣ˡ_._,_ instead. "
    #-}