Data.Nat.Properties

------------------------------------------------------------------------
-- The Agda standard library
--
-- A bunch of properties about natural number operations
------------------------------------------------------------------------

-- See README.Data.Nat for some examples showing how this module can be
-- used.

{-# OPTIONS --without-K --safe #-}

module Data.Nat.Properties where

open import Axiom.UniquenessOfIdentityProofs
open import Algebra.Bundles
open import Algebra.Morphism
open import Algebra.Consequences.Propositional
open import Data.Bool.Base using (Bool; false; true; T)
open import Data.Bool.Properties using (T?)
open import Data.Empty using (⊥)
open import Data.Nat.Base
open import Data.Product using (_×_; _,_)
open import Data.Sum.Base as Sum
open import Data.Unit using (tt)
open import Function.Base
open import Function.Injection using (_↣_)
open import Function.Metric.Nat
open import Level using (0ℓ)
open import Relation.Binary
open import Relation.Binary.Consequences using (flip-Connex)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary hiding (Irrelevant)
open import Relation.Nullary.Decidable using (True; via-injection; map′)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Nullary.Reflects using (fromEquivalence)

open import Algebra.Definitions {A = ℕ} _≡_
  hiding (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Definitions
  using (LeftCancellative; RightCancellative; Cancellative)
open import Algebra.Structures {A = ℕ} _≡_

------------------------------------------------------------------------
-- Properties of _≡_
------------------------------------------------------------------------

suc-injective : ∀ {m n} → suc m ≡ suc n → m ≡ n
suc-injective refl = refl

≡ᵇ⇒≡ : ∀ m n → T (m ≡ᵇ n) → m ≡ n
≡ᵇ⇒≡ zero    zero    _  = refl
≡ᵇ⇒≡ (suc m) (suc n) eq = cong suc (≡ᵇ⇒≡ m n eq)

≡⇒≡ᵇ : ∀ m n → m ≡ n → T (m ≡ᵇ n)
≡⇒≡ᵇ zero    zero    eq = _
≡⇒≡ᵇ (suc m) (suc n) eq = ≡⇒≡ᵇ m n (suc-injective eq)

-- NB: we use the builtin function `_≡ᵇ_` here so that the function
-- quickly decides whether to return `yes` or `no`. It still takes
-- a linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

infix 4 _≟_
_≟_ : Decidable {A = ℕ} _≡_
m ≟ n = map′ (≡ᵇ⇒≡ m n) (≡⇒≡ᵇ m n) (T? (m ≡ᵇ n))

≡-irrelevant : Irrelevant {A = ℕ} _≡_
≡-irrelevant = Decidable⇒UIP.≡-irrelevant _≟_

≟-diag : ∀ {m n} (eq : m ≡ n) → (m ≟ n) ≡ yes eq
≟-diag = ≡-≟-identity _≟_

≡-isDecEquivalence : IsDecEquivalence (_≡_ {A = ℕ})
≡-isDecEquivalence = record
  { isEquivalence = isEquivalence
  ; _≟_           = _≟_
  }

≡-decSetoid : DecSetoid 0ℓ 0ℓ
≡-decSetoid = record
  { Carrier          = ℕ
  ; _≈_              = _≡_
  ; isDecEquivalence = ≡-isDecEquivalence
  }

0≢1+n : ∀ {n} → 0 ≢ suc n
0≢1+n ()

1+n≢0 : ∀ {n} → suc n ≢ 0
1+n≢0 ()

1+n≢n : ∀ {n} → suc n ≢ n
1+n≢n {suc n} = 1+n≢n ∘ suc-injective

------------------------------------------------------------------------
-- Properties of _<ᵇ_
------------------------------------------------------------------------

<ᵇ⇒< : ∀ m n → T (m <ᵇ n) → m < n
<ᵇ⇒< zero    (suc n) m<n = s≤s z≤n
<ᵇ⇒< (suc m) (suc n) m<n = s≤s (<ᵇ⇒< m n m<n)

<⇒<ᵇ : ∀ {m n} → m < n → T (m <ᵇ n)
<⇒<ᵇ (s≤s z≤n)       = tt
<⇒<ᵇ (s≤s (s≤s m<n)) = <⇒<ᵇ (s≤s m<n)

<ᵇ-reflects-< : ∀ m n → Reflects (m < n) (m <ᵇ n)
<ᵇ-reflects-< m n = fromEquivalence (<ᵇ⇒< m n) <⇒<ᵇ

------------------------------------------------------------------------
-- Properties of _≤ᵇ_
------------------------------------------------------------------------

≤ᵇ⇒≤ : ∀ m n → T (m ≤ᵇ n) → m ≤ n
≤ᵇ⇒≤ zero    n m≤n = z≤n
≤ᵇ⇒≤ (suc m) n m≤n = <ᵇ⇒< m n m≤n

≤⇒≤ᵇ : ∀ {m n} → m ≤ n → T (m ≤ᵇ n)
≤⇒≤ᵇ z≤n         = tt
≤⇒≤ᵇ m≤n@(s≤s _) = <⇒<ᵇ m≤n

≤ᵇ-reflects-≤ : ∀ m n → Reflects (m ≤ n) (m ≤ᵇ n)
≤ᵇ-reflects-≤ m n = fromEquivalence (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ

------------------------------------------------------------------------
-- Properties of _≤_
------------------------------------------------------------------------

open import Data.Nat.Properties.Core public

------------------------------------------------------------------------
-- Relational properties of _≤_

≤-reflexive : _≡_ ⇒ _≤_
≤-reflexive {zero}  refl = z≤n
≤-reflexive {suc m} refl = s≤s (≤-reflexive refl)

≤-refl : Reflexive _≤_
≤-refl = ≤-reflexive refl

≤-antisym : Antisymmetric _≡_ _≤_
≤-antisym z≤n       z≤n       = refl
≤-antisym (s≤s m≤n) (s≤s n≤m) = cong suc (≤-antisym m≤n n≤m)

≤-trans : Transitive _≤_
≤-trans z≤n       _         = z≤n
≤-trans (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

≤-total : Total _≤_
≤-total zero    _       = inj₁ z≤n
≤-total _       zero    = inj₂ z≤n
≤-total (suc m) (suc n) with ≤-total m n
... | inj₁ m≤n = inj₁ (s≤s m≤n)
... | inj₂ n≤m = inj₂ (s≤s n≤m)

≤-irrelevant : Irrelevant _≤_
≤-irrelevant z≤n        z≤n        = refl
≤-irrelevant (s≤s m≤n₁) (s≤s m≤n₂) = cong s≤s (≤-irrelevant m≤n₁ m≤n₂)

-- NB: we use the builtin function `_<ᵇ_` here so that the function
-- quickly decides whether to return `yes` or `no`. It still takes
-- a linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

infix 4 _≤?_ _≥?_

_≤?_ : Decidable _≤_
m ≤? n = map′ (≤ᵇ⇒≤ m n) ≤⇒≤ᵇ (T? (m ≤ᵇ n))

_≥?_ : Decidable _≥_
_≥?_ = flip _≤?_

------------------------------------------------------------------------
-- Structures

≤-isPreorder : IsPreorder _≡_ _≤_
≤-isPreorder = record
  { isEquivalence = isEquivalence
  ; reflexive     = ≤-reflexive
  ; trans         = ≤-trans
  }

≤-isPartialOrder : IsPartialOrder _≡_ _≤_
≤-isPartialOrder = record
  { isPreorder = ≤-isPreorder
  ; antisym    = ≤-antisym
  }

≤-isTotalOrder : IsTotalOrder _≡_ _≤_
≤-isTotalOrder = record
  { isPartialOrder = ≤-isPartialOrder
  ; total          = ≤-total
  }

≤-isDecTotalOrder : IsDecTotalOrder _≡_ _≤_
≤-isDecTotalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  ; _≟_          = _≟_
  ; _≤?_         = _≤?_
  }

------------------------------------------------------------------------
-- Bundles

≤-preorder : Preorder 0ℓ 0ℓ 0ℓ
≤-preorder = record
  { isPreorder = ≤-isPreorder
  }

≤-poset : Poset 0ℓ 0ℓ 0ℓ
≤-poset = record
  { isPartialOrder = ≤-isPartialOrder
  }

≤-totalOrder : TotalOrder 0ℓ 0ℓ 0ℓ
≤-totalOrder = record
  { isTotalOrder = ≤-isTotalOrder
  }

≤-decTotalOrder : DecTotalOrder 0ℓ 0ℓ 0ℓ
≤-decTotalOrder = record
  { isDecTotalOrder = ≤-isDecTotalOrder
  }

------------------------------------------------------------------------
-- Other properties of _≤_

s≤s-injective : ∀ {m n} {p q : m ≤ n} → s≤s p ≡ s≤s q → p ≡ q
s≤s-injective refl = refl

≤-step : ∀ {m n} → m ≤ n → m ≤ 1 + n
≤-step z≤n       = z≤n
≤-step (s≤s m≤n) = s≤s (≤-step m≤n)

n≤1+n : ∀ n → n ≤ 1 + n
n≤1+n _ = ≤-step ≤-refl

1+n≰n : ∀ {n} → 1 + n ≰ n
1+n≰n (s≤s le) = 1+n≰n le

n≤0⇒n≡0 : ∀ {n} → n ≤ 0 → n ≡ 0
n≤0⇒n≡0 z≤n = refl

------------------------------------------------------------------------
-- Properties of _<_
------------------------------------------------------------------------

-- Relationships between the various relations

<⇒≤ : _<_ ⇒ _≤_
<⇒≤ (s≤s m≤n) = ≤-trans m≤n (≤-step ≤-refl)

<⇒≢ : _<_ ⇒ _≢_
<⇒≢ m<n refl = 1+n≰n m<n

≤⇒≯ : _≤_ ⇒ _≯_
≤⇒≯ (s≤s m≤n) (s≤s n≤m) = ≤⇒≯ m≤n n≤m

<⇒≱ : _<_ ⇒ _≱_
<⇒≱ (s≤s m+1≤n) (s≤s n≤m) = <⇒≱ m+1≤n n≤m

<⇒≯ : _<_ ⇒ _≯_
<⇒≯ (s≤s m<n) (s≤s n<m) = <⇒≯ m<n n<m

≰⇒≮ : _≰_ ⇒ _≮_
≰⇒≮ m≰n 1+m≤n = m≰n (<⇒≤ 1+m≤n)

≰⇒> : _≰_ ⇒ _>_
≰⇒> {zero}          z≰n = contradiction z≤n z≰n
≰⇒> {suc m} {zero}  _   = s≤s z≤n
≰⇒> {suc m} {suc n} m≰n = s≤s (≰⇒> (m≰n ∘ s≤s))

≰⇒≥ : _≰_ ⇒ _≥_
≰⇒≥ = <⇒≤ ∘ ≰⇒>

≮⇒≥ : _≮_ ⇒ _≥_
≮⇒≥ {_}     {zero}  _       = z≤n
≮⇒≥ {zero}  {suc j} 1≮j+1   = contradiction (s≤s z≤n) 1≮j+1
≮⇒≥ {suc i} {suc j} i+1≮j+1 = s≤s (≮⇒≥ (i+1≮j+1 ∘ s≤s))

≤∧≢⇒< : ∀ {m n} → m ≤ n → m ≢ n → m < n
≤∧≢⇒< {_} {zero}  z≤n       m≢n     = contradiction refl m≢n
≤∧≢⇒< {_} {suc n} z≤n       m≢n     = s≤s z≤n
≤∧≢⇒< {_} {suc n} (s≤s m≤n) 1+m≢1+n =
  s≤s (≤∧≢⇒< m≤n (1+m≢1+n ∘ cong suc))

≤∧≮⇒≡ : ∀ {m n} → m ≤ n → m ≮ n → m ≡ n
≤∧≮⇒≡ m≤n m≮n = ≤-antisym m≤n (≮⇒≥ m≮n)

≤-<-connex : Connex _≤_ _<_
≤-<-connex m n with m ≤? n
... | yes m≤n = inj₁ m≤n
... | no ¬m≤n = inj₂ (≰⇒> ¬m≤n)

≥->-connex : Connex _≥_ _>_
≥->-connex = flip ≤-<-connex

<-≤-connex : Connex _<_ _≤_
<-≤-connex = flip-Connex ≤-<-connex

>-≥-connex : Connex _>_ _≥_
>-≥-connex = flip-Connex ≥->-connex

------------------------------------------------------------------------
-- Relational properties of _<_

<-irrefl : Irreflexive _≡_ _<_
<-irrefl refl (s≤s n<n) = <-irrefl refl n<n

<-asym : Asymmetric _<_
<-asym (s≤s n<m) (s≤s m<n) = <-asym n<m m<n

<-trans : Transitive _<_
<-trans (s≤s i≤j) (s≤s j<k) = s≤s (≤-trans i≤j (≤-trans (n≤1+n _) j<k))

<-transʳ : Trans _≤_ _<_ _<_
<-transʳ m≤n (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

<-transˡ : Trans _<_ _≤_ _<_
<-transˡ (s≤s m≤n) (s≤s n≤o) = s≤s (≤-trans m≤n n≤o)

-- NB: we use the builtin function `_<ᵇ_` here so that the function
-- quickly decides which constructor to return. It still takes a
-- linear amount of time to generate the proof if it is inspected.
-- We expect the main benefit to be visible in compiled code as the
-- backend erases proofs.

<-cmp : Trichotomous _≡_ _<_
<-cmp m n with m ≟ n | T? (m <ᵇ n)
... | yes m≡n | _       = tri≈ (<-irrefl m≡n) m≡n (<-irrefl (sym m≡n))
... | no  m≢n | yes m<n = tri< (<ᵇ⇒< m n m<n) m≢n (<⇒≯ (<ᵇ⇒< m n m<n))
... | no  m≢n | no  m≮n = tri> (m≮n ∘ <⇒<ᵇ)   m≢n (≤∧≢⇒< (≮⇒≥ (m≮n ∘ <⇒<ᵇ)) (m≢n ∘ sym))

infix 4 _<?_ _>?_

_<?_ : Decidable _<_
m <? n = suc m ≤? n

_>?_ : Decidable _>_
_>?_ = flip _<?_

<-irrelevant : Irrelevant _<_
<-irrelevant = ≤-irrelevant

<-resp₂-≡ : _<_ Respects₂ _≡_
<-resp₂-≡ = subst (_ <_) , subst (_< _)

------------------------------------------------------------------------
-- Bundles

<-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
<-isStrictPartialOrder = record
  { isEquivalence = isEquivalence
  ; irrefl        = <-irrefl
  ; trans         = <-trans
  ; <-resp-≈      = <-resp₂-≡
  }

<-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
<-isStrictTotalOrder = record
  { isEquivalence = isEquivalence
  ; trans         = <-trans
  ; compare       = <-cmp
  }

<-strictPartialOrder : StrictPartialOrder 0ℓ 0ℓ 0ℓ
<-strictPartialOrder = record
  { isStrictPartialOrder = <-isStrictPartialOrder
  }

<-strictTotalOrder : StrictTotalOrder 0ℓ 0ℓ 0ℓ
<-strictTotalOrder = record
  { isStrictTotalOrder = <-isStrictTotalOrder
  }

------------------------------------------------------------------------
-- Other properties of _<_

n≮n : ∀ n → n ≮ n
n≮n n = <-irrefl (refl {x = n})

0<1+n : ∀ {n} → 0 < suc n
0<1+n = s≤s z≤n

n<1+n : ∀ n → n < suc n
n<1+n n = ≤-refl

n≢0⇒n>0 : ∀ {n} → n ≢ 0 → n > 0
n≢0⇒n>0 {zero}  0≢0 =  contradiction refl 0≢0
n≢0⇒n>0 {suc n} _   =  0<1+n

m<n⇒n≢0 : ∀ {m n} → m < n → n ≢ 0
m<n⇒n≢0 (s≤s m≤n) ()

m<n⇒m≤1+n : ∀ {m n} → m < n → m ≤ suc n
m<n⇒m≤1+n (s≤s z≤n)       = z≤n
m<n⇒m≤1+n (s≤s (s≤s m<n)) = s≤s (m<n⇒m≤1+n (s≤s m<n))

∀[m≤n⇒m≢o]⇒n<o : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒n<o _       zero    m≤n⇒n≢0 = contradiction refl (m≤n⇒n≢0 z≤n)
∀[m≤n⇒m≢o]⇒n<o zero    (suc o) _       = 0<1+n
∀[m≤n⇒m≢o]⇒n<o (suc n) (suc o) m≤n⇒n≢o = s≤s (∀[m≤n⇒m≢o]⇒n<o n o rec)
  where
  rec : ∀ {m} → m ≤ n → m ≢ o
  rec m≤n refl = m≤n⇒n≢o (s≤s m≤n) refl

∀[m<n⇒m≢o]⇒n≤o : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒n≤o zero    n       _       = z≤n
∀[m<n⇒m≢o]⇒n≤o (suc n) zero    m<n⇒m≢0 = contradiction refl (m<n⇒m≢0 0<1+n)
∀[m<n⇒m≢o]⇒n≤o (suc n) (suc o) m<n⇒m≢o = s≤s (∀[m<n⇒m≢o]⇒n≤o n o rec)
  where
  rec : ∀ {m} → m < n → m ≢ o
  rec x<m refl = m<n⇒m≢o (s≤s x<m) refl

------------------------------------------------------------------------
-- A module for reasoning about the _≤_ and _<_ relations
------------------------------------------------------------------------

module ≤-Reasoning where
  open import Relation.Binary.Reasoning.Base.Triple
    ≤-isPreorder
    <-trans
    (resp₂ _<_)
    <⇒≤
    <-transˡ
    <-transʳ
    public
    hiding (step-≈; step-≈˘)

open ≤-Reasoning

------------------------------------------------------------------------
-- Properties of _+_
------------------------------------------------------------------------

+-suc : ∀ m n → m + suc n ≡ suc (m + n)
+-suc zero    n = refl
+-suc (suc m) n = cong suc (+-suc m n)

------------------------------------------------------------------------
-- Algebraic properties of _+_

+-assoc : Associative _+_
+-assoc zero    _ _ = refl
+-assoc (suc m) n o = cong suc (+-assoc m n o)

+-identityˡ : LeftIdentity 0 _+_
+-identityˡ _ = refl

+-identityʳ : RightIdentity 0 _+_
+-identityʳ zero    = refl
+-identityʳ (suc n) = cong suc (+-identityʳ n)

+-identity : Identity 0 _+_
+-identity = +-identityˡ , +-identityʳ

+-comm : Commutative _+_
+-comm zero    n = sym (+-identityʳ n)
+-comm (suc m) n = begin-equality
  suc m + n   ≡⟨⟩
  suc (m + n) ≡⟨ cong suc (+-comm m n) ⟩
  suc (n + m) ≡⟨ sym (+-suc n m) ⟩
  n + suc m   ∎

+-cancelˡ-≡ : LeftCancellative _≡_ _+_
+-cancelˡ-≡ zero    eq = eq
+-cancelˡ-≡ (suc m) eq = +-cancelˡ-≡ m (cong pred eq)

+-cancelʳ-≡ : RightCancellative _≡_ _+_
+-cancelʳ-≡ = comm+cancelˡ⇒cancelʳ +-comm +-cancelˡ-≡

+-cancel-≡ : Cancellative _≡_ _+_
+-cancel-≡ = +-cancelˡ-≡ , +-cancelʳ-≡

------------------------------------------------------------------------
-- Structures

+-isMagma : IsMagma _+_
+-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _+_
  }

+-isSemigroup : IsSemigroup _+_
+-isSemigroup = record
  { isMagma = +-isMagma
  ; assoc   = +-assoc
  }

+-isCommutativeSemigroup : IsCommutativeSemigroup _+_
+-isCommutativeSemigroup = record
  { isSemigroup = +-isSemigroup
  ; comm        = +-comm
  }

+-0-isMonoid : IsMonoid _+_ 0
+-0-isMonoid = record
  { isSemigroup = +-isSemigroup
  ; identity    = +-identity
  }

+-0-isCommutativeMonoid : IsCommutativeMonoid _+_ 0
+-0-isCommutativeMonoid = record
  { isMonoid = +-0-isMonoid
  ; comm     = +-comm
  }

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

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

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

------------------------------------------------------------------------
-- Bundles

+-magma : Magma 0ℓ 0ℓ
+-magma = record
  { isMagma = +-isMagma
  }

+-semigroup : Semigroup 0ℓ 0ℓ
+-semigroup = record
  { isSemigroup = +-isSemigroup
  }

+-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
+-commutativeSemigroup = record
  { isCommutativeSemigroup = +-isCommutativeSemigroup
  }

+-0-monoid : Monoid 0ℓ 0ℓ
+-0-monoid = record
  { isMonoid = +-0-isMonoid
  }

+-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
+-0-commutativeMonoid = record
  { isCommutativeMonoid = +-0-isCommutativeMonoid
  }

∸-magma : Magma 0ℓ 0ℓ
∸-magma = magma _∸_


------------------------------------------------------------------------
-- Other properties of _+_ and _≡_

m≢1+m+n : ∀ m {n} → m ≢ suc (m + n)
m≢1+m+n (suc m) eq = m≢1+m+n m (cong pred eq)

m≢1+n+m : ∀ m {n} → m ≢ suc (n + m)
m≢1+n+m m m≡1+n+m = m≢1+m+n m (trans m≡1+n+m (cong suc (+-comm _ m)))

m+1+n≢m : ∀ m {n} → m + suc n ≢ m
m+1+n≢m (suc m) = (m+1+n≢m m) ∘ suc-injective

m+1+n≢0 : ∀ m {n} → m + suc n ≢ 0
m+1+n≢0 m {n} rewrite +-suc m n = λ()

m+n≡0⇒m≡0 : ∀ m {n} → m + n ≡ 0 → m ≡ 0
m+n≡0⇒m≡0 zero eq = refl

m+n≡0⇒n≡0 : ∀ m {n} → m + n ≡ 0 → n ≡ 0
m+n≡0⇒n≡0 m {n} m+n≡0 = m+n≡0⇒m≡0 n (trans (+-comm n m) (m+n≡0))

------------------------------------------------------------------------
-- Properties of _+_ and _≤_/_<_

+-cancelˡ-≤ : LeftCancellative _≤_ _+_
+-cancelˡ-≤ zero    le       = le
+-cancelˡ-≤ (suc m) (s≤s le) = +-cancelˡ-≤ m le

+-cancelʳ-≤ : RightCancellative _≤_ _+_
+-cancelʳ-≤ {m} n o le =
  +-cancelˡ-≤ m (subst₂ _≤_ (+-comm n m) (+-comm o m) le)

+-cancel-≤ : Cancellative _≤_ _+_
+-cancel-≤ = +-cancelˡ-≤ , +-cancelʳ-≤

+-cancelˡ-< : LeftCancellative _<_ _+_
+-cancelˡ-< m {n} {o} = +-cancelˡ-≤ m ∘ subst (_≤ m + o) (sym (+-suc m n))

+-cancelʳ-< : RightCancellative _<_ _+_
+-cancelʳ-< n o n+m<o+m = +-cancelʳ-≤ (suc n) o n+m<o+m

+-cancel-< : Cancellative _<_ _+_
+-cancel-< = +-cancelˡ-< , +-cancelʳ-<

≤-stepsˡ : ∀ {m n} o → m ≤ n → m ≤ o + n
≤-stepsˡ zero    m≤n = m≤n
≤-stepsˡ (suc o) m≤n = ≤-step (≤-stepsˡ o m≤n)

≤-stepsʳ : ∀ {m n} o → m ≤ n → m ≤ n + o
≤-stepsʳ {m} o m≤n = subst (m ≤_) (+-comm o _) (≤-stepsˡ o m≤n)

m≤m+n : ∀ m n → m ≤ m + n
m≤m+n zero    n = z≤n
m≤m+n (suc m) n = s≤s (m≤m+n m n)

m≤n+m : ∀ m n → m ≤ n + m
m≤n+m m n = subst (m ≤_) (+-comm m n) (m≤m+n m n)

m≤n⇒m<n∨m≡n :  ∀ {m n} → m ≤ n → m < n ⊎ m ≡ n
m≤n⇒m<n∨m≡n {0}     {0}     _          =  inj₂ refl
m≤n⇒m<n∨m≡n {0}     {suc n} _          =  inj₁ 0<1+n
m≤n⇒m<n∨m≡n {suc m} {suc n} (s≤s m≤n)  with m≤n⇒m<n∨m≡n m≤n
... | inj₂ m≡n = inj₂ (cong suc m≡n)
... | inj₁ m<n = inj₁ (s≤s m<n)

m+n≤o⇒m≤o : ∀ m {n o} → m + n ≤ o → m ≤ o
m+n≤o⇒m≤o zero    m+n≤o       = z≤n
m+n≤o⇒m≤o (suc m) (s≤s m+n≤o) = s≤s (m+n≤o⇒m≤o m m+n≤o)

m+n≤o⇒n≤o : ∀ m {n o} → m + n ≤ o → n ≤ o
m+n≤o⇒n≤o zero    n≤o   = n≤o
m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)

+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+-mono-≤ {_} {m} z≤n       o≤p = ≤-trans o≤p (m≤n+m _ m)
+-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)

+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
+-monoˡ-≤ n m≤o = +-mono-≤ m≤o (≤-refl {n})

+-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
+-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o

+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
+-mono-<-≤ {_} {suc n} (s≤s z≤n)       o≤p = s≤s (≤-stepsˡ n o≤p)
+-mono-<-≤ {_} {_}     (s≤s (s≤s m<n)) o≤p = s≤s (+-mono-<-≤ (s≤s m<n) o≤p)

+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
+-mono-≤-< {_} {n} z≤n       o<p = ≤-trans o<p (m≤n+m _ n)
+-mono-≤-< {_} {_} (s≤s m≤n) o<p = s≤s (+-mono-≤-< m≤n o<p)

+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+-mono-< m≤n = +-mono-≤-< (<⇒≤ m≤n)

+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
+-monoˡ-< n = +-monoˡ-≤ n

+-monoʳ-< : ∀ n → (n +_) Preserves _<_ ⟶ _<_
+-monoʳ-< zero    m≤o = m≤o
+-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)

m+1+n≰m : ∀ m {n} → m + suc n ≰ m
m+1+n≰m (suc m) le = m+1+n≰m m (≤-pred le)

m<m+n : ∀ m {n} → n > 0 → m < m + n
m<m+n zero    n>0 = n>0
m<m+n (suc m) n>0 = s≤s (m<m+n m n>0)

m<n+m : ∀ m {n} → n > 0 → m < n + m
m<n+m m {n} n>0 rewrite +-comm n m = m<m+n m n>0

m+n≮n : ∀ m n → m + n ≮ n
m+n≮n zero    n                   = n≮n n
m+n≮n (suc m) (suc n) (s≤s m+n<n) = m+n≮n m (suc n) (≤-step m+n<n)

m+n≮m : ∀ m n → m + n ≮ m
m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)

------------------------------------------------------------------------
-- Properties of _*_
------------------------------------------------------------------------

*-suc : ∀ m n → m * suc n ≡ m + m * n
*-suc zero    n = refl
*-suc (suc m) n = begin-equality
  suc m * suc n         ≡⟨⟩
  suc n + m * suc n     ≡⟨ cong (suc n +_) (*-suc m n) ⟩
  suc n + (m + m * n)   ≡⟨⟩
  suc (n + (m + m * n)) ≡⟨ cong suc (sym (+-assoc n m (m * n))) ⟩
  suc (n + m + m * n)   ≡⟨ cong (λ x → suc (x + m * n)) (+-comm n m) ⟩
  suc (m + n + m * n)   ≡⟨ cong suc (+-assoc m n (m * n)) ⟩
  suc (m + (n + m * n)) ≡⟨⟩
  suc m + suc m * n     ∎

------------------------------------------------------------------------
-- Algebraic properties of _*_

*-identityˡ : LeftIdentity 1 _*_
*-identityˡ n = +-identityʳ n

*-identityʳ : RightIdentity 1 _*_
*-identityʳ zero    = refl
*-identityʳ (suc n) = cong suc (*-identityʳ n)

*-identity : Identity 1 _*_
*-identity = *-identityˡ , *-identityʳ

*-zeroˡ : LeftZero 0 _*_
*-zeroˡ _ = refl

*-zeroʳ : RightZero 0 _*_
*-zeroʳ zero    = refl
*-zeroʳ (suc n) = *-zeroʳ n

*-zero : Zero 0 _*_
*-zero = *-zeroˡ , *-zeroʳ

*-comm : Commutative _*_
*-comm zero    n = sym (*-zeroʳ n)
*-comm (suc m) n = begin-equality
  suc m * n  ≡⟨⟩
  n + m * n  ≡⟨ cong (n +_) (*-comm m n) ⟩
  n + n * m  ≡⟨ sym (*-suc n m) ⟩
  n * suc m  ∎

*-distribʳ-+ : _*_ DistributesOverʳ _+_
*-distribʳ-+ m zero    o = refl
*-distribʳ-+ m (suc n) o = begin-equality
  (suc n + o) * m     ≡⟨⟩
  m + (n + o) * m     ≡⟨ cong (m +_) (*-distribʳ-+ m n o) ⟩
  m + (n * m + o * m) ≡⟨ sym (+-assoc m (n * m) (o * m)) ⟩
  m + n * m + o * m   ≡⟨⟩
  suc n * m + o * m   ∎

*-distribˡ-+ : _*_ DistributesOverˡ _+_
*-distribˡ-+ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-+

*-distrib-+ : _*_ DistributesOver _+_
*-distrib-+ = *-distribˡ-+ , *-distribʳ-+

*-assoc : Associative _*_
*-assoc zero    n o = refl
*-assoc (suc m) n o = begin-equality
  (suc m * n) * o     ≡⟨⟩
  (n + m * n) * o     ≡⟨ *-distribʳ-+ o n (m * n) ⟩
  n * o + (m * n) * o ≡⟨ cong (n * o +_) (*-assoc m n o) ⟩
  n * o + m * (n * o) ≡⟨⟩
  suc m * (n * o)     ∎

------------------------------------------------------------------------
-- Structures

*-isMagma : IsMagma _*_
*-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _*_
  }

*-isSemigroup : IsSemigroup _*_
*-isSemigroup = record
  { isMagma = *-isMagma
  ; assoc   = *-assoc
  }

*-isCommutativeSemigroup : IsCommutativeSemigroup _*_
*-isCommutativeSemigroup = record
  { isSemigroup = *-isSemigroup
  ; comm        = *-comm
  }

*-1-isMonoid : IsMonoid _*_ 1
*-1-isMonoid = record
  { isSemigroup = *-isSemigroup
  ; identity    = *-identity
  }

*-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1
*-1-isCommutativeMonoid = record
  { isMonoid = *-1-isMonoid
  ; comm     = *-comm
  }

+-*-isSemiring : IsSemiring _+_ _*_ 0 1
+-*-isSemiring = record
  { isSemiringWithoutAnnihilatingZero = record
    { +-isCommutativeMonoid = +-0-isCommutativeMonoid
    ; *-isMonoid            = *-1-isMonoid
    ; distrib               = *-distrib-+
    }
  ; zero = *-zero
  }

+-*-isCommutativeSemiring : IsCommutativeSemiring _+_ _*_ 0 1
+-*-isCommutativeSemiring = record
  { isSemiring = +-*-isSemiring
  ; *-comm     = *-comm
  }

------------------------------------------------------------------------
-- Bundles

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

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

*-magma : Magma 0ℓ 0ℓ
*-magma = record
  { isMagma = *-isMagma
  }

*-semigroup : Semigroup 0ℓ 0ℓ
*-semigroup = record
  { isSemigroup = *-isSemigroup
  }

*-commutativeSemigroup : CommutativeSemigroup 0ℓ 0ℓ
*-commutativeSemigroup = record
  { isCommutativeSemigroup = *-isCommutativeSemigroup
  }

*-1-monoid : Monoid 0ℓ 0ℓ
*-1-monoid = record
  { isMonoid = *-1-isMonoid
  }

*-1-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
*-1-commutativeMonoid = record
  { isCommutativeMonoid = *-1-isCommutativeMonoid
  }

+-*-semiring : Semiring 0ℓ 0ℓ
+-*-semiring = record
  { isSemiring = +-*-isSemiring
  }

+-*-commutativeSemiring : CommutativeSemiring 0ℓ 0ℓ
+-*-commutativeSemiring = record
  { isCommutativeSemiring = +-*-isCommutativeSemiring
  }

------------------------------------------------------------------------
-- Other properties of _*_ and _≡_

*-cancelʳ-≡ : ∀ m n {o} → m * suc o ≡ n * suc o → m ≡ n
*-cancelʳ-≡ zero    zero        eq = refl
*-cancelʳ-≡ (suc m) (suc n) {o} eq =
  cong suc (*-cancelʳ-≡ m n (+-cancelˡ-≡ (suc o) eq))

*-cancelˡ-≡ : ∀ {m n} o → suc o * m ≡ suc o * n → m ≡ n
*-cancelˡ-≡ {m} {n} o eq = *-cancelʳ-≡ m n
  (subst₂ _≡_ (*-comm (suc o) m) (*-comm (suc o) n) eq)

m*n≡0⇒m≡0∨n≡0 : ∀ m {n} → m * n ≡ 0 → m ≡ 0 ⊎ n ≡ 0
m*n≡0⇒m≡0∨n≡0 zero    {n}     eq = inj₁ refl
m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  eq = inj₂ refl

m*n≡1⇒m≡1 : ∀ m n → m * n ≡ 1 → m ≡ 1
m*n≡1⇒m≡1 (suc zero)    n             _  = refl
m*n≡1⇒m≡1 (suc (suc m)) (suc zero)    ()
m*n≡1⇒m≡1 (suc (suc m)) zero          eq =
  contradiction (trans (sym $ *-zeroʳ m) eq) λ()

m*n≡1⇒n≡1 : ∀ m n → m * n ≡ 1 → n ≡ 1
m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)

------------------------------------------------------------------------
-- Other properties of _*_ and _≤_/_<_

*-cancelʳ-≤ : ∀ m n o → m * suc o ≤ n * suc o → m ≤ n
*-cancelʳ-≤ zero    _       _ _  = z≤n
*-cancelʳ-≤ (suc m) (suc n) o le =
  s≤s (*-cancelʳ-≤ m n o (+-cancelˡ-≤ (suc o) le))

*-cancelˡ-≤ : ∀ {m n} o → suc o * m ≤ suc o * n → m ≤ n
*-cancelˡ-≤ {m} {n} o rewrite *-comm (suc o) m | *-comm (suc o) n = *-cancelʳ-≤ m n o

*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
*-mono-≤ z≤n       _   = z≤n
*-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)

*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})

*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o

*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
*-mono-< (s≤s z≤n)       (s≤s u≤v) = s≤s z≤n
*-mono-< (s≤s (s≤s m≤n)) (s≤s u≤v) =
  +-mono-< (s≤s u≤v) (*-mono-< (s≤s m≤n) (s≤s u≤v))

*-monoˡ-< : ∀ n → (_* suc n) Preserves _<_ ⟶ _<_
*-monoˡ-< n (s≤s z≤n)       = s≤s z≤n
*-monoˡ-< n (s≤s (s≤s m≤o)) =
  +-mono-≤-< (≤-refl {suc n}) (*-monoˡ-< n (s≤s m≤o))

*-monoʳ-< : ∀ n → (suc n *_) Preserves _<_ ⟶ _<_
*-monoʳ-< zero    (s≤s m≤o) = +-mono-≤ (s≤s m≤o) z≤n
*-monoʳ-< (suc n) (s≤s m≤o) =
  +-mono-≤ (s≤s m≤o) (<⇒≤ (*-monoʳ-< n (s≤s m≤o)))

m≤m*n : ∀ m {n} → 0 < n → m ≤ m * n
m≤m*n m {n} 0<n = begin
  m     ≡⟨ sym (*-identityʳ m) ⟩
  m * 1 ≤⟨ *-monoʳ-≤ m 0<n ⟩
  m * n ∎

m<m*n :  ∀ {m n} → 0 < m → 1 < n → m < m * n
m<m*n {m@(suc m-1)} {n@(suc (suc n-2))} (s≤s _) (s≤s (s≤s _)) = begin-strict
  m           <⟨ s≤s (s≤s (m≤n+m m-1 n-2)) ⟩
  n + m-1     ≤⟨ +-monoʳ-≤ n (m≤m*n m-1 0<1+n) ⟩
  n + m-1 * n ≡⟨⟩
  m * n       ∎

*-cancelʳ-< : RightCancellative _<_ _*_
*-cancelʳ-< {zero}  zero    (suc o) _     = 0<1+n
*-cancelʳ-< {suc m} zero    (suc o) _     = 0<1+n
*-cancelʳ-< {m}     (suc n) (suc o) nm<om =
  s≤s (*-cancelʳ-< n o (+-cancelˡ-< m nm<om))

-- Redo in terms of `comm+cancelʳ⇒cancelˡ` when generalised
*-cancelˡ-< : LeftCancellative _<_ _*_
*-cancelˡ-< x {y} {z} rewrite *-comm x y | *-comm x z = *-cancelʳ-< y z

*-cancel-< : Cancellative _<_ _*_
*-cancel-< = *-cancelˡ-< , *-cancelʳ-<

------------------------------------------------------------------------
-- Properties of _^_
------------------------------------------------------------------------

^-identityʳ : RightIdentity 1 _^_
^-identityʳ zero    = refl
^-identityʳ (suc n) = cong suc (^-identityʳ n)

^-zeroˡ : LeftZero 1 _^_
^-zeroˡ zero    = refl
^-zeroˡ (suc n) = begin-equality
  1 ^ suc n   ≡⟨⟩
  1 * (1 ^ n) ≡⟨ *-identityˡ (1 ^ n) ⟩
  1 ^ n       ≡⟨ ^-zeroˡ n ⟩
  1           ∎

^-distribˡ-+-* : ∀ m n o → m ^ (n + o) ≡ m ^ n * m ^ o
^-distribˡ-+-* m zero    o = sym (+-identityʳ (m ^ o))
^-distribˡ-+-* m (suc n) o = begin-equality
  m * (m ^ (n + o))       ≡⟨ cong (m *_) (^-distribˡ-+-* m n o) ⟩
  m * ((m ^ n) * (m ^ o)) ≡⟨ sym (*-assoc m _ _) ⟩
  (m * (m ^ n)) * (m ^ o) ∎

^-semigroup-morphism : ∀ {n} → (n ^_) Is +-semigroup -Semigroup⟶ *-semigroup
^-semigroup-morphism = record
  { ⟦⟧-cong = cong (_ ^_)
  ; ∙-homo  = ^-distribˡ-+-* _
  }

^-monoid-morphism : ∀ {n} → (n ^_) Is +-0-monoid -Monoid⟶ *-1-monoid
^-monoid-morphism = record
  { sm-homo = ^-semigroup-morphism
  ; ε-homo  = refl
  }

^-*-assoc : ∀ m n o → (m ^ n) ^ o ≡ m ^ (n * o)
^-*-assoc m n zero    = cong (m ^_) (sym $ *-zeroʳ n)
^-*-assoc m n (suc o) = begin-equality
  (m ^ n) * ((m ^ n) ^ o) ≡⟨ cong ((m ^ n) *_) (^-*-assoc m n o) ⟩
  (m ^ n) * (m ^ (n * o)) ≡⟨ sym (^-distribˡ-+-* m n (n * o)) ⟩
  m ^ (n + n * o)         ≡⟨ cong (m ^_) (sym (*-suc n o)) ⟩
  m ^ (n * (suc o)) ∎

m^n≡0⇒m≡0 : ∀ m n → m ^ n ≡ 0 → m ≡ 0
m^n≡0⇒m≡0 m (suc n) eq = [ id , m^n≡0⇒m≡0 m n ]′ (m*n≡0⇒m≡0∨n≡0 m eq)

m^n≡1⇒n≡0∨m≡1 : ∀ m n → m ^ n ≡ 1 → n ≡ 0 ⊎ m ≡ 1
m^n≡1⇒n≡0∨m≡1 m zero    _  = inj₁ refl
m^n≡1⇒n≡0∨m≡1 m (suc n) eq = inj₂ (m*n≡1⇒m≡1 m (m ^ n) eq)

------------------------------------------------------------------------
-- Properties of _⊔_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Algebraic properties

⊔-assoc : Associative _⊔_
⊔-assoc zero    _       _       = refl
⊔-assoc (suc m) zero    o       = refl
⊔-assoc (suc m) (suc n) zero    = refl
⊔-assoc (suc m) (suc n) (suc o) = cong suc $ ⊔-assoc m n o

⊔-identityˡ : LeftIdentity 0 _⊔_
⊔-identityˡ _ = refl

⊔-identityʳ : RightIdentity 0 _⊔_
⊔-identityʳ zero    = refl
⊔-identityʳ (suc n) = refl

⊔-identity : Identity 0 _⊔_
⊔-identity = ⊔-identityˡ , ⊔-identityʳ

⊔-comm : Commutative _⊔_
⊔-comm zero    n       = sym $ ⊔-identityʳ n
⊔-comm (suc m) zero    = refl
⊔-comm (suc m) (suc n) = cong suc (⊔-comm m n)

⊔-sel : Selective _⊔_
⊔-sel zero    _    = inj₂ refl
⊔-sel (suc m) zero = inj₁ refl
⊔-sel (suc m) (suc n) with ⊔-sel m n
... | inj₁ m⊔n≡m = inj₁ (cong suc m⊔n≡m)
... | inj₂ m⊔n≡n = inj₂ (cong suc m⊔n≡n)

⊔-idem : Idempotent _⊔_
⊔-idem = sel⇒idem ⊔-sel

⊔-least : ∀ {m n o} → m ≤ o → n ≤ o → m ⊔ n ≤ o
⊔-least {m} {n} m≤o n≤o with ⊔-sel m n
... | inj₁ m⊔n≡m rewrite m⊔n≡m = m≤o
... | inj₂ m⊔n≡n rewrite m⊔n≡n = n≤o

------------------------------------------------------------------------
-- Structures

⊔-isMagma : IsMagma _⊔_
⊔-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _⊔_
  }

⊔-isSemigroup : IsSemigroup _⊔_
⊔-isSemigroup = record
  { isMagma = ⊔-isMagma
  ; assoc   = ⊔-assoc
  }

⊔-isBand : IsBand _⊔_
⊔-isBand = record
  { isSemigroup = ⊔-isSemigroup
  ; idem        = ⊔-idem
  }

⊔-isSemilattice : IsSemilattice _⊔_
⊔-isSemilattice = record
  { isBand = ⊔-isBand
  ; comm   = ⊔-comm
  }

⊔-0-isMonoid : IsMonoid _⊔_ 0
⊔-0-isMonoid = record
  { isSemigroup = ⊔-isSemigroup
  ; identity = ⊔-identity
  }

⊔-0-isCommutativeMonoid : IsCommutativeMonoid _⊔_ 0
⊔-0-isCommutativeMonoid = record
  { isMonoid = ⊔-0-isMonoid
  ; comm = ⊔-comm
  }

------------------------------------------------------------------------
-- Bundles

⊔-magma : Magma 0ℓ 0ℓ
⊔-magma = record
  { isMagma = ⊔-isMagma
  }

⊔-semigroup : Semigroup 0ℓ 0ℓ
⊔-semigroup = record
  { isSemigroup = ⊔-isSemigroup
  }

⊔-band : Band 0ℓ 0ℓ
⊔-band = record
  { isBand = ⊔-isBand
  }

⊔-semilattice : Semilattice 0ℓ 0ℓ
⊔-semilattice = record
  { isSemilattice = ⊔-isSemilattice
  }

⊔-0-commutativeMonoid : CommutativeMonoid 0ℓ 0ℓ
⊔-0-commutativeMonoid = record
  { isCommutativeMonoid = ⊔-0-isCommutativeMonoid
  }

------------------------------------------------------------------------
-- Other properties of _⊔_ and _≡_

⊔-triangulate : ∀ m n o → m ⊔ n ⊔ o ≡ (m ⊔ n) ⊔ (n ⊔ o)
⊔-triangulate m n o = begin-equality
  m ⊔ n ⊔ o           ≡⟨ cong (λ v → m ⊔ v ⊔ o) (sym (⊔-idem n)) ⟩
  m ⊔ (n ⊔ n) ⊔ o     ≡⟨ ⊔-assoc m _ _ ⟩
  m ⊔ ((n ⊔ n) ⊔ o)   ≡⟨ cong (m ⊔_) (⊔-assoc n _ _) ⟩
  m ⊔ (n ⊔ (n ⊔ o))   ≡⟨ sym (⊔-assoc m _ _) ⟩
  (m ⊔ n) ⊔ (n ⊔ o)   ∎

------------------------------------------------------------------------
-- Other properties of _⊔_ and _≤_/_<_

m≤m⊔n : ∀ m n → m ≤ m ⊔ n
m≤m⊔n zero    _       = z≤n
m≤m⊔n (suc m) zero    = ≤-refl
m≤m⊔n (suc m) (suc n) = s≤s $ m≤m⊔n m n

n≤m⊔n : ∀ m n → n ≤ m ⊔ n
n≤m⊔n m n = subst (n ≤_) (⊔-comm n m) (m≤m⊔n n m)

m≤n⇒n⊔m≡n : ∀ {m n} → m ≤ n → n ⊔ m ≡ n
m≤n⇒n⊔m≡n z≤n       = ⊔-identityʳ _
m≤n⇒n⊔m≡n (s≤s m≤n) = cong suc (m≤n⇒n⊔m≡n m≤n)

m≤n⇒m⊔n≡n : ∀ {m n} → m ≤ n → m ⊔ n ≡ n
m≤n⇒m⊔n≡n {m} m≤n = trans (⊔-comm m _) (m≤n⇒n⊔m≡n m≤n)

n⊔m≡m⇒n≤m : ∀ {m n} → n ⊔ m ≡ m → n ≤ m
n⊔m≡m⇒n≤m n⊔m≡m = subst (_ ≤_) n⊔m≡m (m≤m⊔n _ _)

n⊔m≡n⇒m≤n : ∀ {m n} → n ⊔ m ≡ n → m ≤ n
n⊔m≡n⇒m≤n n⊔m≡n = subst (_ ≤_) n⊔m≡n (n≤m⊔n _ _)

m≤n⇒m≤n⊔o : ∀ {m n} o → m ≤ n → m ≤ n ⊔ o
m≤n⇒m≤n⊔o o m≤n = ≤-trans m≤n (m≤m⊔n _ o)

m≤n⇒m≤o⊔n : ∀ {m n} o → m ≤ n → m ≤ o ⊔ n
m≤n⇒m≤o⊔n n m≤n = ≤-trans m≤n (n≤m⊔n n _)

m⊔n≤o⇒m≤o : ∀ m n {o} → m ⊔ n ≤ o → m ≤ o
m⊔n≤o⇒m≤o m n m⊔n≤o = ≤-trans (m≤m⊔n m n) m⊔n≤o

m⊔n≤o⇒n≤o : ∀ m n {o} → m ⊔ n ≤ o → n ≤ o
m⊔n≤o⇒n≤o m n m⊔n≤o = ≤-trans (n≤m⊔n m n) m⊔n≤o

m<n⇒m<n⊔o : ∀ {m n} o → m < n → m < n ⊔ o
m<n⇒m<n⊔o = m≤n⇒m≤n⊔o

m<n⇒m<o⊔n : ∀ {m n} o → m < n → m < o ⊔ n
m<n⇒m<o⊔n = m≤n⇒m≤o⊔n

m⊔n<o⇒m<o : ∀ m n {o} → m ⊔ n < o → m < o
m⊔n<o⇒m<o m n m⊔n<o = <-transʳ (m≤m⊔n m n) m⊔n<o

m⊔n<o⇒n<o : ∀ m n {o} → m ⊔ n < o → n < o
m⊔n<o⇒n<o m n m⊔n<o = <-transʳ (n≤m⊔n m n) m⊔n<o

⊔-mono-≤ : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
⊔-mono-≤ {m} {n} {u} {v} m≤n u≤v with ⊔-sel m u
... | inj₁ m⊔u≡m rewrite m⊔u≡m = ≤-trans m≤n (m≤m⊔n n v)
... | inj₂ m⊔u≡u rewrite m⊔u≡u = ≤-trans u≤v (n≤m⊔n n v)

⊔-monoˡ-≤ : ∀ n → (_⊔ n) Preserves _≤_ ⟶ _≤_
⊔-monoˡ-≤ n m≤o = ⊔-mono-≤ m≤o (≤-refl {n})

⊔-monoʳ-≤ : ∀ n → (n ⊔_) Preserves _≤_ ⟶ _≤_
⊔-monoʳ-≤ n m≤o = ⊔-mono-≤ (≤-refl {n}) m≤o

⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊔-mono-< = ⊔-mono-≤

⊔-pres-≤m : ∀ {m n o} → n ≤ m → o ≤ m → n ⊔ o ≤ m
⊔-pres-≤m {m} n≤m o≤m = subst (_ ≤_) (⊔-idem m) (⊔-mono-≤ n≤m o≤m)

⊔-pres-<m : ∀ {m n o} → n < m → o < m → n ⊔ o < m
⊔-pres-<m {m} n<m o<m = subst (_ <_) (⊔-idem m) (⊔-mono-< n<m o<m)

------------------------------------------------------------------------
-- Other properties of _⊔_ and _+_

+-distribˡ-⊔ : _+_ DistributesOverˡ _⊔_
+-distribˡ-⊔ zero    n o = refl
+-distribˡ-⊔ (suc m) n o = cong suc (+-distribˡ-⊔ m n o)

+-distribʳ-⊔ : _+_ DistributesOverʳ _⊔_
+-distribʳ-⊔ = comm+distrˡ⇒distrʳ +-comm +-distribˡ-⊔

+-distrib-⊔ : _+_ DistributesOver _⊔_
+-distrib-⊔ = +-distribˡ-⊔ , +-distribʳ-⊔

m⊔n≤m+n : ∀ m n → m ⊔ n ≤ m + n
m⊔n≤m+n m n with ⊔-sel m n
... | inj₁ m⊔n≡m rewrite m⊔n≡m = m≤m+n m n
... | inj₂ m⊔n≡n rewrite m⊔n≡n = m≤n+m n m

------------------------------------------------------------------------
-- Other properties of _⊔_ and _*_

*-distribˡ-⊔ : _*_ DistributesOverˡ _⊔_
*-distribˡ-⊔ m zero o = sym (cong (_⊔ m * o) (*-zeroʳ m))
*-distribˡ-⊔ m (suc n) zero = begin-equality
  m * (suc n ⊔ zero)         ≡⟨⟩
  m * suc n                  ≡˘⟨ ⊔-identityʳ (m * suc n) ⟩
  m * suc n ⊔ zero           ≡˘⟨ cong (m * suc n ⊔_) (*-zeroʳ m) ⟩
  m * suc n ⊔ m * zero       ∎
*-distribˡ-⊔ m (suc n) (suc o) = begin-equality
  m * (suc n ⊔ suc o)        ≡⟨⟩
  m * suc (n ⊔ o)            ≡⟨ *-suc m (n ⊔ o) ⟩
  m + m * (n ⊔ o)            ≡⟨ cong (m +_) (*-distribˡ-⊔ m n o) ⟩
  m + (m * n ⊔ m * o)        ≡⟨ +-distribˡ-⊔ m (m * n) (m * o) ⟩
  (m + m * n) ⊔ (m + m * o)  ≡˘⟨ cong₂ _⊔_ (*-suc m n) (*-suc m o) ⟩
  (m * suc n) ⊔ (m * suc o)  ∎

*-distribʳ-⊔ : _*_ DistributesOverʳ _⊔_
*-distribʳ-⊔ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-⊔

*-distrib-⊔ : _*_ DistributesOver _⊔_
*-distrib-⊔ = *-distribˡ-⊔ , *-distribʳ-⊔

------------------------------------------------------------------------
-- Properties of _⊓_
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Algebraic properties

⊓-assoc : Associative _⊓_
⊓-assoc zero    _       _       = refl
⊓-assoc (suc m) zero    o       = refl
⊓-assoc (suc m) (suc n) zero    = refl
⊓-assoc (suc m) (suc n) (suc o) = cong suc $ ⊓-assoc m n o

⊓-zeroˡ : LeftZero 0 _⊓_
⊓-zeroˡ _ = refl

⊓-zeroʳ : RightZero 0 _⊓_
⊓-zeroʳ zero    = refl
⊓-zeroʳ (suc n) = refl

⊓-zero : Zero 0 _⊓_
⊓-zero = ⊓-zeroˡ , ⊓-zeroʳ

⊓-comm : Commutative _⊓_
⊓-comm zero    n       = sym $ ⊓-zeroʳ n
⊓-comm (suc m) zero    = refl
⊓-comm (suc m) (suc n) = cong suc (⊓-comm m n)

⊓-sel : Selective _⊓_
⊓-sel zero    _    = inj₁ refl
⊓-sel (suc m) zero = inj₂ refl
⊓-sel (suc m) (suc n) with ⊓-sel m n
... | inj₁ m⊓n≡m = inj₁ (cong suc m⊓n≡m)
... | inj₂ m⊓n≡n = inj₂ (cong suc m⊓n≡n)

⊓-idem : Idempotent _⊓_
⊓-idem = sel⇒idem ⊓-sel

⊓-greatest : ∀ {m n o} → m ≥ o → n ≥ o → m ⊓ n ≥ o
⊓-greatest {m} {n} m≥o n≥o with ⊓-sel m n
... | inj₁ m⊓n≡m rewrite m⊓n≡m = m≥o
... | inj₂ m⊓n≡n rewrite m⊓n≡n = n≥o

⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_
⊓-distribʳ-⊔ (suc m) (suc n) (suc o) = cong suc $ ⊓-distribʳ-⊔ m n o
⊓-distribʳ-⊔ (suc m) (suc n) zero    = cong suc $ refl
⊓-distribʳ-⊔ (suc m) zero    o       = refl
⊓-distribʳ-⊔ zero    n       o       = begin-equality
  (n ⊔ o) ⊓ 0    ≡⟨ ⊓-comm (n ⊔ o) 0 ⟩
  0 ⊓ (n ⊔ o)    ≡⟨⟩
  0 ⊓ n ⊔ 0 ⊓ o  ≡⟨ ⊓-comm 0 n ⟨ cong₂ _⊔_ ⟩ ⊓-comm 0 o ⟩
  n ⊓ 0 ⊔ o ⊓ 0  ∎

⊓-distribˡ-⊔ : _⊓_ DistributesOverˡ _⊔_
⊓-distribˡ-⊔ = comm+distrʳ⇒distrˡ ⊓-comm ⊓-distribʳ-⊔

⊓-distrib-⊔ : _⊓_ DistributesOver _⊔_
⊓-distrib-⊔ = ⊓-distribˡ-⊔ , ⊓-distribʳ-⊔

⊔-abs-⊓ : _⊔_ Absorbs _⊓_
⊔-abs-⊓ zero    n       = refl
⊔-abs-⊓ (suc m) zero    = refl
⊔-abs-⊓ (suc m) (suc n) = cong suc $ ⊔-abs-⊓ m n

⊓-abs-⊔ : _⊓_ Absorbs _⊔_
⊓-abs-⊔ zero    n       = refl
⊓-abs-⊔ (suc m) (suc n) = cong suc $ ⊓-abs-⊔ m n
⊓-abs-⊔ (suc m) zero    = cong suc $ begin-equality
  m ⊓ m       ≡⟨ cong (m ⊓_) $ sym $ ⊔-identityʳ m ⟩
  m ⊓ (m ⊔ 0) ≡⟨ ⊓-abs-⊔ m zero ⟩
  m           ∎

⊓-⊔-absorptive : Absorptive _⊓_ _⊔_
⊓-⊔-absorptive = ⊓-abs-⊔ , ⊔-abs-⊓

------------------------------------------------------------------------
-- Structures

⊓-isMagma : IsMagma _⊓_
⊓-isMagma = record
  { isEquivalence = isEquivalence
  ; ∙-cong        = cong₂ _⊓_
  }

⊓-isSemigroup : IsSemigroup _⊓_
⊓-isSemigroup = record
  { isMagma = ⊓-isMagma
  ; assoc   = ⊓-assoc
  }

⊓-isBand : IsBand _⊓_
⊓-isBand = record
  { isSemigroup = ⊓-isSemigroup
  ; idem        = ⊓-idem
  }

⊓-isSemilattice : IsSemilattice _⊓_
⊓-isSemilattice = record
  { isBand = ⊓-isBand
  ; comm   = ⊓-comm
  }

⊔-⊓-isSemiringWithoutOne : IsSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isSemiringWithoutOne = record
  { +-isCommutativeMonoid = ⊔-0-isCommutativeMonoid
  ; *-isSemigroup         = ⊓-isSemigroup
  ; distrib               = ⊓-distrib-⊔
  ; zero                  = ⊓-zero
  }

⊔-⊓-isCommutativeSemiringWithoutOne
  : IsCommutativeSemiringWithoutOne _⊔_ _⊓_ 0
⊔-⊓-isCommutativeSemiringWithoutOne = record
  { isSemiringWithoutOne = ⊔-⊓-isSemiringWithoutOne
  ; *-comm               = ⊓-comm
  }

⊓-⊔-isLattice : IsLattice _⊓_ _⊔_
⊓-⊔-isLattice = record
  { isEquivalence = isEquivalence
  ; ∨-comm        = ⊓-comm
  ; ∨-assoc       = ⊓-assoc
  ; ∨-cong        = cong₂ _⊓_
  ; ∧-comm        = ⊔-comm
  ; ∧-assoc       = ⊔-assoc
  ; ∧-cong        = cong₂ _⊔_
  ; absorptive    = ⊓-⊔-absorptive
  }

⊓-⊔-isDistributiveLattice : IsDistributiveLattice _⊓_ _⊔_
⊓-⊔-isDistributiveLattice = record
  { isLattice    = ⊓-⊔-isLattice
  ; ∨-distribʳ-∧ = ⊓-distribʳ-⊔
  }

------------------------------------------------------------------------
-- Bundles

⊓-magma : Magma 0ℓ 0ℓ
⊓-magma = record
  { isMagma = ⊓-isMagma
  }

⊓-semigroup : Semigroup 0ℓ 0ℓ
⊓-semigroup = record
  { isSemigroup = ⊔-isSemigroup
  }

⊓-band : Band 0ℓ 0ℓ
⊓-band = record
  { isBand = ⊓-isBand
  }

⊓-semilattice : Semilattice 0ℓ 0ℓ
⊓-semilattice = record
  { isSemilattice = ⊓-isSemilattice
  }

⊔-⊓-commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne 0ℓ 0ℓ
⊔-⊓-commutativeSemiringWithoutOne = record
  { isCommutativeSemiringWithoutOne =
      ⊔-⊓-isCommutativeSemiringWithoutOne
  }

⊓-⊔-lattice : Lattice 0ℓ 0ℓ
⊓-⊔-lattice = record
  { isLattice = ⊓-⊔-isLattice
  }

⊓-⊔-distributiveLattice : DistributiveLattice 0ℓ 0ℓ
⊓-⊔-distributiveLattice = record
  { isDistributiveLattice = ⊓-⊔-isDistributiveLattice
  }

------------------------------------------------------------------------
-- Other properties of _⊓_ and _≡_

⊓-triangulate : ∀ m n o → m ⊓ n ⊓ o ≡ (m ⊓ n) ⊓ (n ⊓ o)
⊓-triangulate m n o = begin-equality
  m ⊓ n ⊓ o           ≡⟨ sym (cong (λ v → m ⊓ v ⊓ o) (⊓-idem n)) ⟩
  m ⊓ (n ⊓ n) ⊓ o     ≡⟨ ⊓-assoc m _ _ ⟩
  m ⊓ ((n ⊓ n) ⊓ o)   ≡⟨ cong (m ⊓_) (⊓-assoc n _ _) ⟩
  m ⊓ (n ⊓ (n ⊓ o))   ≡⟨ sym (⊓-assoc m _ _) ⟩
  (m ⊓ n) ⊓ (n ⊓ o)   ∎

------------------------------------------------------------------------
-- Other properties of _⊓_ and _≤_/_<_

m⊓n≤m : ∀ m n → m ⊓ n ≤ m
m⊓n≤m zero    _       = z≤n
m⊓n≤m (suc m) zero    = z≤n
m⊓n≤m (suc m) (suc n) = s≤s $ m⊓n≤m m n

m⊓n≤n : ∀ m n → m ⊓ n ≤ n
m⊓n≤n m n = subst (_≤ n) (⊓-comm n m) (m⊓n≤m n m)

m≤n⇒m⊓n≡m : ∀ {m n} → m ≤ n → m ⊓ n ≡ m
m≤n⇒m⊓n≡m z≤n       = refl
m≤n⇒m⊓n≡m (s≤s m≤n) = cong suc (m≤n⇒m⊓n≡m m≤n)

m≤n⇒n⊓m≡m : ∀ {m n} → m ≤ n → n ⊓ m ≡ m
m≤n⇒n⊓m≡m {m} m≤n = trans (⊓-comm _ m) (m≤n⇒m⊓n≡m m≤n)

m⊓n≡m⇒m≤n : ∀ {m n} → m ⊓ n ≡ m → m ≤ n
m⊓n≡m⇒m≤n m⊓n≡m = subst (_≤ _) m⊓n≡m (m⊓n≤n _ _)

m⊓n≡n⇒n≤m : ∀ {m n} → m ⊓ n ≡ n → n ≤ m
m⊓n≡n⇒n≤m m⊓n≡n = subst (_≤ _) m⊓n≡n (m⊓n≤m _ _)

m≤n⇒m⊓o≤n : ∀ {m n} o → m ≤ n → m ⊓ o ≤ n
m≤n⇒m⊓o≤n o m≤n = ≤-trans (m⊓n≤m _ o) m≤n

m≤n⇒o⊓m≤n : ∀ {m n} o → m ≤ n → o ⊓ m ≤ n
m≤n⇒o⊓m≤n n m≤n = ≤-trans (m⊓n≤n n _) m≤n

m≤n⊓o⇒m≤n : ∀ {m} n o → m ≤ n ⊓ o → m ≤ n
m≤n⊓o⇒m≤n n o m≤n⊓o = ≤-trans m≤n⊓o (m⊓n≤m n o)

m≤n⊓o⇒m≤o : ∀ {m} n o → m ≤ n ⊓ o → m ≤ o
m≤n⊓o⇒m≤o n o m≤n⊓o = ≤-trans m≤n⊓o (m⊓n≤n n o)

m<n⇒m⊓o<n : ∀ {m n} o → m < n → m ⊓ o < n
m<n⇒m⊓o<n o m<n = <-transʳ (m⊓n≤m _ o) m<n

m<n⇒o⊓m<n : ∀ {m n} o → m < n → o ⊓ m < n
m<n⇒o⊓m<n o m<n = <-transʳ (m⊓n≤n o _) m<n

m<n⊓o⇒m<n : ∀ {m} n o → m < n ⊓ o → m < n
m<n⊓o⇒m<n = m≤n⊓o⇒m≤n

m<n⊓o⇒m<o : ∀ {m} n o → m < n ⊓ o → m < o
m<n⊓o⇒m<o = m≤n⊓o⇒m≤o

⊓-mono-≤ : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
⊓-mono-≤ {m} {n} {u} {v} m≤n u≤v with ⊓-sel n v
... | inj₁ n⊓v≡n rewrite n⊓v≡n = ≤-trans (m⊓n≤m m u) m≤n
... | inj₂ n⊓v≡v rewrite n⊓v≡v = ≤-trans (m⊓n≤n m u) u≤v

⊓-monoˡ-≤ : ∀ n → (_⊓ n) Preserves _≤_ ⟶ _≤_
⊓-monoˡ-≤ n m≤o = ⊓-mono-≤ m≤o (≤-refl {n})

⊓-monoʳ-≤ : ∀ n → (n ⊓_) Preserves _≤_ ⟶ _≤_
⊓-monoʳ-≤ n m≤o = ⊓-mono-≤ (≤-refl {n}) m≤o

⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
⊓-mono-< = ⊓-mono-≤

m⊓n≤m⊔n : ∀ m n → m ⊓ n ≤ m ⊔ n
m⊓n≤m⊔n zero    n       = z≤n
m⊓n≤m⊔n (suc m) zero    = z≤n
m⊓n≤m⊔n (suc m) (suc n) = s≤s (m⊓n≤m⊔n m n)

⊓-pres-m≤ : ∀ {m n o} → m ≤ n → m ≤ o → m ≤ n ⊓ o
⊓-pres-m≤ {m} m≤n m≤o = subst (_≤ _) (⊓-idem m) (⊓-mono-≤ m≤n m≤o)

⊓-pres-m< : ∀ {m n o} → m < n → m < o → m < n ⊓ o
⊓-pres-m< {m} m<n m<o = subst (_< _) (⊓-idem m) (⊓-mono-< m<n m<o)

------------------------------------------------------------------------
-- Other properties of _⊓_ and _+_

+-distribˡ-⊓ : _+_ DistributesOverˡ _⊓_
+-distribˡ-⊓ zero    n o = refl
+-distribˡ-⊓ (suc m) n o = cong suc (+-distribˡ-⊓ m n o)

+-distribʳ-⊓ : _+_ DistributesOverʳ _⊓_
+-distribʳ-⊓ = comm+distrˡ⇒distrʳ +-comm +-distribˡ-⊓

+-distrib-⊓ : _+_ DistributesOver _⊓_
+-distrib-⊓ = +-distribˡ-⊓ , +-distribʳ-⊓

m⊓n≤m+n : ∀ m n → m ⊓ n ≤ m + n
m⊓n≤m+n m n with ⊓-sel m n
... | inj₁ m⊓n≡m rewrite m⊓n≡m = m≤m+n m n
... | inj₂ m⊓n≡n rewrite m⊓n≡n = m≤n+m n m

------------------------------------------------------------------------
-- Other properties of _⊓_ and _*_

*-distribˡ-⊓ : _*_ DistributesOverˡ _⊓_
*-distribˡ-⊓ m 0 o = begin-equality
  m * (0 ⊓ o)               ≡⟨⟩
  m * 0                     ≡⟨ *-zeroʳ m ⟩
  0                         ≡⟨⟩
  0 ⊓ (m * o)               ≡˘⟨ cong (_⊓ (m * o)) (*-zeroʳ m) ⟩
  (m * 0) ⊓ (m * o)         ∎
*-distribˡ-⊓ m (suc n) 0 = begin-equality
  m * (suc n ⊓ 0)           ≡⟨⟩
  m * 0                     ≡⟨ *-zeroʳ m ⟩
  0                         ≡˘⟨ ⊓-zeroʳ (m * suc n) ⟩
  (m * suc n) ⊓ 0           ≡˘⟨ cong (m * suc n ⊓_) (*-zeroʳ m) ⟩
  (m * suc n) ⊓ (m * 0)     ∎
*-distribˡ-⊓ m (suc n) (suc o) = begin-equality
  m * (suc n ⊓ suc o)       ≡⟨⟩
  m * suc (n ⊓ o)           ≡⟨ *-suc m (n ⊓ o) ⟩
  m + m * (n ⊓ o)           ≡⟨ cong (m +_) (*-distribˡ-⊓ m n o) ⟩
  m + (m * n) ⊓ (m * o)     ≡⟨ +-distribˡ-⊓ m (m * n) (m * o) ⟩
  (m + m * n) ⊓ (m + m * o) ≡˘⟨ cong₂ _⊓_ (*-suc m n) (*-suc m o) ⟩
  (m * suc n) ⊓ (m * suc o) ∎

*-distribʳ-⊓ : _*_ DistributesOverʳ _⊓_
*-distribʳ-⊓ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-⊓

*-distrib-⊓ : _*_ DistributesOver _⊓_
*-distrib-⊓ = *-distribˡ-⊓ , *-distribʳ-⊓

------------------------------------------------------------------------
-- Properties of _∸_
------------------------------------------------------------------------

0∸n≡0 : LeftZero zero _∸_
0∸n≡0 zero    = refl
0∸n≡0 (suc _) = refl

n∸n≡0 : ∀ n → n ∸ n ≡ 0
n∸n≡0 zero    = refl
n∸n≡0 (suc n) = n∸n≡0 n

------------------------------------------------------------------------
-- Properties of _∸_ and pred

pred[m∸n]≡m∸[1+n] : ∀ m n → pred (m ∸ n) ≡ m ∸ suc n
pred[m∸n]≡m∸[1+n] zero    zero    = refl
pred[m∸n]≡m∸[1+n] (suc m) zero    = refl
pred[m∸n]≡m∸[1+n] zero (suc n)    = refl
pred[m∸n]≡m∸[1+n] (suc m) (suc n) = pred[m∸n]≡m∸[1+n] m n

------------------------------------------------------------------------
-- Properties of _∸_ and _≤_/_<_

m∸n≤m : ∀ m n → m ∸ n ≤ m
m∸n≤m n       zero    = ≤-refl
m∸n≤m zero    (suc n) = ≤-refl
m∸n≤m (suc m) (suc n) = ≤-trans (m∸n≤m m n) (n≤1+n m)

m≮m∸n : ∀ m n → m ≮ m ∸ n
m≮m∸n m       zero    = n≮n m
m≮m∸n (suc m) (suc n) = m≮m∸n m n ∘ ≤-trans (n≤1+n (suc m))

1+m≢m∸n : ∀ {m} n → suc m ≢ m ∸ n
1+m≢m∸n {m} n eq = m≮m∸n m n (≤-reflexive eq)

∸-mono : _∸_ Preserves₂ _≤_ ⟶ _≥_ ⟶ _≤_
∸-mono z≤n         (s≤s n₁≥n₂)    = z≤n
∸-mono (s≤s m₁≤m₂) (s≤s n₁≥n₂)    = ∸-mono m₁≤m₂ n₁≥n₂
∸-mono m₁≤m₂       (z≤n {n = n₁}) = ≤-trans (m∸n≤m _ n₁) m₁≤m₂

∸-monoˡ-≤ : ∀ {m n} o → m ≤ n → m ∸ o ≤ n ∸ o
∸-monoˡ-≤ o m≤n = ∸-mono {u = o} m≤n ≤-refl

∸-monoʳ-≤ : ∀ {m n} o → m ≤ n → o ∸ m ≥ o ∸ n
∸-monoʳ-≤ _ m≤n = ∸-mono ≤-refl m≤n

∸-monoʳ-< : ∀ {m n o} → o < n → n ≤ m → m ∸ n < m ∸ o
∸-monoʳ-< {n = suc n} {zero}  (s≤s o<n) (s≤s n<m) = s≤s (m∸n≤m _ n)
∸-monoʳ-< {n = suc n} {suc o} (s≤s o<n) (s≤s n<m) = ∸-monoʳ-< o<n n<m

∸-cancelʳ-≤ : ∀ {m n o} → m ≤ o → o ∸ n ≤ o ∸ m → m ≤ n
∸-cancelʳ-≤ {_}     {_}     z≤n       _       = z≤n
∸-cancelʳ-≤ {suc m} {zero}  (s≤s _)   o<o∸m   = contradiction o<o∸m (m≮m∸n _ m)
∸-cancelʳ-≤ {suc m} {suc n} (s≤s m≤o) o∸n<o∸m = s≤s (∸-cancelʳ-≤ m≤o o∸n<o∸m)

∸-cancelʳ-< : ∀ {m n o} → o ∸ m < o ∸ n → n < m
∸-cancelʳ-< {zero}  {n}     {o}     o<o∸n   = contradiction o<o∸n (m≮m∸n o n)
∸-cancelʳ-< {suc m} {zero}  {_}     o∸n<o∸m = 0<1+n
∸-cancelʳ-< {suc m} {suc n} {suc o} o∸n<o∸m = s≤s (∸-cancelʳ-< o∸n<o∸m)

∸-cancelˡ-≡ :  ∀ {m n o} → n ≤ m → o ≤ m → m ∸ n ≡ m ∸ o → n ≡ o
∸-cancelˡ-≡ {_}         z≤n       z≤n       _  = refl
∸-cancelˡ-≡ {o = suc o} z≤n       (s≤s _)   eq = contradiction eq (1+m≢m∸n o)
∸-cancelˡ-≡ {n = suc n} (s≤s _)   z≤n       eq = contradiction (sym eq) (1+m≢m∸n n)
∸-cancelˡ-≡ {_}         (s≤s n≤m) (s≤s o≤m) eq = cong suc (∸-cancelˡ-≡ n≤m o≤m eq)

∸-cancelʳ-≡ :  ∀ {m n o} → o ≤ m → o ≤ n → m ∸ o ≡ n ∸ o → m ≡ n
∸-cancelʳ-≡  z≤n       z≤n      eq = eq
∸-cancelʳ-≡ (s≤s o≤m) (s≤s o≤n) eq = cong suc (∸-cancelʳ-≡ o≤m o≤n eq)

m∸n≡0⇒m≤n : ∀ {m n} → m ∸ n ≡ 0 → m ≤ n
m∸n≡0⇒m≤n {zero}  {_}    _   = z≤n
m∸n≡0⇒m≤n {suc m} {suc n} eq = s≤s (m∸n≡0⇒m≤n eq)

m≤n⇒m∸n≡0 : ∀ {m n} → m ≤ n → m ∸ n ≡ 0
m≤n⇒m∸n≡0 {n = n} z≤n      = 0∸n≡0 n
m≤n⇒m∸n≡0 {_}    (s≤s m≤n) = m≤n⇒m∸n≡0 m≤n

m<n⇒0<n∸m : ∀ {m n} → m < n → 0 < n ∸ m
m<n⇒0<n∸m {zero}  {suc n} _         = 0<1+n
m<n⇒0<n∸m {suc m} {suc n} (s≤s m<n) = m<n⇒0<n∸m m<n

m∸n≢0⇒n<m : ∀ {m n} → m ∸ n ≢ 0 → n < m
m∸n≢0⇒n<m {m} {n} m∸n≢0 with n <? m
... | yes n<m = n<m
... | no  n≮m = contradiction (m≤n⇒m∸n≡0 (≮⇒≥ n≮m)) m∸n≢0

m>n⇒m∸n≢0 : ∀ {m n} → m > n → m ∸ n ≢ 0
m>n⇒m∸n≢0 {n = suc n} (s≤s m>n) = m>n⇒m∸n≢0 m>n

---------------------------------------------------------------
-- Properties of _∸_ and _+_

+-∸-comm : ∀ {m} n {o} → o ≤ m → (m + n) ∸ o ≡ (m ∸ o) + n
+-∸-comm {zero}  _ {zero}  _         = refl
+-∸-comm {suc m} _ {zero}  _         = refl
+-∸-comm {suc m} n {suc o} (s≤s o≤m) = +-∸-comm n o≤m

∸-+-assoc : ∀ m n o → (m ∸ n) ∸ o ≡ m ∸ (n + o)
∸-+-assoc zero zero o = refl
∸-+-assoc zero (suc n) o = 0∸n≡0 o
∸-+-assoc (suc m) zero o = refl
∸-+-assoc (suc m) (suc n) o = ∸-+-assoc m n o

+-∸-assoc : ∀ m {n o} → o ≤ n → (m + n) ∸ o ≡ m + (n ∸ o)
+-∸-assoc m (z≤n {n = n})             = begin-equality m + n ∎
+-∸-assoc m (s≤s {m = o} {n = n} o≤n) = begin-equality
  (m + suc n) ∸ suc o  ≡⟨ cong (_∸ suc o) (+-suc m n) ⟩
  suc (m + n) ∸ suc o  ≡⟨⟩
  (m + n) ∸ o          ≡⟨ +-∸-assoc m o≤n ⟩
  m + (n ∸ o)          ∎

m≤n+m∸n : ∀ m n → m ≤ n + (m ∸ n)
m≤n+m∸n zero    n       = z≤n
m≤n+m∸n (suc m) zero    = ≤-refl
m≤n+m∸n (suc m) (suc n) = s≤s (m≤n+m∸n m n)

m+n∸n≡m : ∀ m n → m + n ∸ n ≡ m
m+n∸n≡m m n = begin-equality
  (m + n) ∸ n  ≡⟨ +-∸-assoc m (≤-refl {x = n}) ⟩
  m + (n ∸ n)  ≡⟨ cong (m +_) (n∸n≡0 n) ⟩
  m + 0        ≡⟨ +-identityʳ m ⟩
  m            ∎

m+n∸m≡n : ∀ m n → m + n ∸ m ≡ n
m+n∸m≡n m n = trans (cong (_∸ m) (+-comm m n)) (m+n∸n≡m n m)

m+[n∸m]≡n : ∀ {m n} → m ≤ n → m + (n ∸ m) ≡ n
m+[n∸m]≡n {m} {n} m≤n = begin-equality
  m + (n ∸ m)  ≡⟨ sym $ +-∸-assoc m m≤n ⟩
  (m + n) ∸ m  ≡⟨ cong (_∸ m) (+-comm m n) ⟩
  (n + m) ∸ m  ≡⟨ m+n∸n≡m n m ⟩
  n            ∎

m∸n+n≡m : ∀ {m n} → n ≤ m → (m ∸ n) + n ≡ m
m∸n+n≡m {m} {n} n≤m = begin-equality
  (m ∸ n) + n ≡⟨ sym (+-∸-comm n n≤m) ⟩
  (m + n) ∸ n ≡⟨ m+n∸n≡m m n ⟩
  m           ∎

m∸[m∸n]≡n : ∀ {m n} → n ≤ m → m ∸ (m ∸ n) ≡ n
m∸[m∸n]≡n {m}     {_}     z≤n       = n∸n≡0 m
m∸[m∸n]≡n {suc m} {suc n} (s≤s n≤m) = begin-equality
  suc m ∸ (m ∸ n)   ≡⟨ +-∸-assoc 1 (m∸n≤m m n) ⟩
  suc (m ∸ (m ∸ n)) ≡⟨ cong suc (m∸[m∸n]≡n n≤m) ⟩
  suc n             ∎

[m+n]∸[m+o]≡n∸o : ∀ m n o → (m + n) ∸ (m + o) ≡ n ∸ o
[m+n]∸[m+o]≡n∸o zero    n o = refl
[m+n]∸[m+o]≡n∸o (suc m) n o = [m+n]∸[m+o]≡n∸o m n o

------------------------------------------------------------------------
-- Properties of _∸_ and _*_

*-distribʳ-∸ : _*_ DistributesOverʳ _∸_
*-distribʳ-∸ m       zero    zero    = refl
*-distribʳ-∸ zero    zero    (suc o) = sym (0∸n≡0 (o * zero))
*-distribʳ-∸ (suc m) zero    (suc o) = refl
*-distribʳ-∸ m       (suc n) zero    = refl
*-distribʳ-∸ m       (suc n) (suc o) = begin-equality
  (n ∸ o) * m             ≡⟨ *-distribʳ-∸ m n o ⟩
  n * m ∸ o * m           ≡⟨ sym $ [m+n]∸[m+o]≡n∸o m _ _ ⟩
  m + n * m ∸ (m + o * m) ∎

*-distribˡ-∸ : _*_ DistributesOverˡ _∸_
*-distribˡ-∸ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-∸

*-distrib-∸ : _*_ DistributesOver _∸_
*-distrib-∸ = *-distribˡ-∸ , *-distribʳ-∸

even≢odd :  ∀ m n → 2 * m ≢ suc (2 * n)
even≢odd (suc m) zero    eq = contradiction (suc-injective eq) (m+1+n≢0 m)
even≢odd (suc m) (suc n) eq = even≢odd m n (suc-injective (begin-equality
  suc (2 * m)         ≡⟨ sym (+-suc m _) ⟩
  m + suc (m + 0)     ≡⟨ suc-injective eq ⟩
  suc n + suc (n + 0) ≡⟨ cong suc (+-suc n _) ⟩
  suc (suc (2 * n))   ∎))

------------------------------------------------------------------------
-- Properties of _∸_ and _⊓_ and _⊔_

m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero    n       = refl
m⊓n+n∸m≡n (suc m) zero    = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n

[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
[m∸n]⊓[n∸m]≡0 zero zero       = refl
[m∸n]⊓[n∸m]≡0 zero (suc n)    = refl
[m∸n]⊓[n∸m]≡0 (suc m) zero    = refl
[m∸n]⊓[n∸m]≡0 (suc m) (suc n) = [m∸n]⊓[n∸m]≡0 m n

∸-distribˡ-⊓-⊔ : ∀ m n o → m ∸ (n ⊓ o) ≡ (m ∸ n) ⊔ (m ∸ o)
∸-distribˡ-⊓-⊔ m       zero    zero    = sym (⊔-idem m)
∸-distribˡ-⊓-⊔ zero    zero    (suc o) = refl
∸-distribˡ-⊓-⊔ zero    (suc n) zero    = refl
∸-distribˡ-⊓-⊔ zero    (suc n) (suc o) = refl
∸-distribˡ-⊓-⊔ (suc m) (suc n) zero    = sym (m≤n⇒m⊔n≡n (≤-step (m∸n≤m m n)))
∸-distribˡ-⊓-⊔ (suc m) zero    (suc o) = sym (m≤n⇒n⊔m≡n (≤-step (m∸n≤m m o)))
∸-distribˡ-⊓-⊔ (suc m) (suc n) (suc o) = ∸-distribˡ-⊓-⊔ m n o

∸-distribʳ-⊓ : _∸_ DistributesOverʳ _⊓_
∸-distribʳ-⊓ zero    n       o       = refl
∸-distribʳ-⊓ (suc m) zero    o       = refl
∸-distribʳ-⊓ (suc m) (suc n) zero    = sym (⊓-zeroʳ (n ∸ m))
∸-distribʳ-⊓ (suc m) (suc n) (suc o) = ∸-distribʳ-⊓ m n o

∸-distribˡ-⊔-⊓ : ∀ m n o → m ∸ (n ⊔ o) ≡ (m ∸ n) ⊓ (m ∸ o)
∸-distribˡ-⊔-⊓ m       zero    zero    = sym (⊓-idem m)
∸-distribˡ-⊔-⊓ zero    zero    o       = 0∸n≡0 o
∸-distribˡ-⊔-⊓ zero    (suc n) o       = 0∸n≡0 (suc n ⊔ o)
∸-distribˡ-⊔-⊓ (suc m) (suc n) zero    = sym (m≤n⇒m⊓n≡m (≤-step (m∸n≤m m n)))
∸-distribˡ-⊔-⊓ (suc m) zero    (suc o) = sym (m≤n⇒n⊓m≡m (≤-step (m∸n≤m m o)))
∸-distribˡ-⊔-⊓ (suc m) (suc n) (suc o) = ∸-distribˡ-⊔-⊓ m n o

∸-distribʳ-⊔ : _∸_ DistributesOverʳ _⊔_
∸-distribʳ-⊔ zero    n       o       = refl
∸-distribʳ-⊔ (suc m) zero    o       = refl
∸-distribʳ-⊔ (suc m) (suc n) zero    = sym (⊔-identityʳ (n ∸ m))
∸-distribʳ-⊔ (suc m) (suc n) (suc o) = ∸-distribʳ-⊔ m n o

------------------------------------------------------------------------
-- Properties of pred
------------------------------------------------------------------------

pred-mono : pred Preserves _≤_ ⟶ _≤_
pred-mono m≤n = ∸-mono m≤n (≤-refl {1})

≤pred⇒≤ : ∀ {m n} → m ≤ pred n → m ≤ n
≤pred⇒≤ {m} {zero}  le = le
≤pred⇒≤ {m} {suc n} le = ≤-step le

≤⇒pred≤ : ∀ {m n} → m ≤ n → pred m ≤ n
≤⇒pred≤ {zero}  le = le
≤⇒pred≤ {suc m} le = ≤-trans (n≤1+n m) le

<⇒≤pred : ∀ {m n} → m < n → m ≤ pred n
<⇒≤pred (s≤s le) = le

suc[pred[n]]≡n : ∀ {n} → n ≢ 0 → suc (pred n) ≡ n
suc[pred[n]]≡n {zero}  n≢0 = contradiction refl n≢0
suc[pred[n]]≡n {suc n} n≢0 = refl

------------------------------------------------------------------------
-- Properties of ∣_-_∣
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Basic

m≡n⇒∣m-n∣≡0 : ∀ {m n} → m ≡ n → ∣ m - n ∣ ≡ 0
m≡n⇒∣m-n∣≡0 {zero}  refl = refl
m≡n⇒∣m-n∣≡0 {suc m} refl = m≡n⇒∣m-n∣≡0 {m} refl

∣m-n∣≡0⇒m≡n : ∀ {m n} → ∣ m - n ∣ ≡ 0 → m ≡ n
∣m-n∣≡0⇒m≡n {zero}  {zero}  eq = refl
∣m-n∣≡0⇒m≡n {suc m} {suc n} eq = cong suc (∣m-n∣≡0⇒m≡n eq)

m≤n⇒∣n-m∣≡n∸m : ∀ {m n} → m ≤ n → ∣ n - m ∣ ≡ n ∸ m
m≤n⇒∣n-m∣≡n∸m {_} {zero}  z≤n       = refl
m≤n⇒∣n-m∣≡n∸m {_} {suc m} z≤n       = refl
m≤n⇒∣n-m∣≡n∸m {_} {_}     (s≤s m≤n) = m≤n⇒∣n-m∣≡n∸m m≤n

∣m-n∣≡m∸n⇒n≤m : ∀ {m n} → ∣ m - n ∣ ≡ m ∸ n → n ≤ m
∣m-n∣≡m∸n⇒n≤m {zero}  {zero}  eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {zero}  eq = z≤n
∣m-n∣≡m∸n⇒n≤m {suc m} {suc n} eq = s≤s (∣m-n∣≡m∸n⇒n≤m eq)

∣n-n∣≡0 : ∀ n → ∣ n - n ∣ ≡ 0
∣n-n∣≡0 n = m≡n⇒∣m-n∣≡0 {n} refl

∣m-m+n∣≡n : ∀ m n → ∣ m - m + n ∣ ≡ n
∣m-m+n∣≡n zero    n = refl
∣m-m+n∣≡n (suc m) n = ∣m-m+n∣≡n m n

∣m+n-m+o∣≡∣n-o| : ∀ m n o → ∣ m + n - m + o ∣ ≡ ∣ n - o ∣
∣m+n-m+o∣≡∣n-o| zero    n o = refl
∣m+n-m+o∣≡∣n-o| (suc m) n o = ∣m+n-m+o∣≡∣n-o| m n o

m∸n≤∣m-n∣ : ∀ m n → m ∸ n ≤ ∣ m - n ∣
m∸n≤∣m-n∣ m n with ≤-total m n
... | inj₁ m≤n = subst (_≤ ∣ m - n ∣) (sym (m≤n⇒m∸n≡0 m≤n)) z≤n
... | inj₂ n≤m = subst (m ∸ n ≤_) (sym (m≤n⇒∣n-m∣≡n∸m n≤m)) ≤-refl

∣m-n∣≤m⊔n : ∀ m n → ∣ m - n ∣ ≤ m ⊔ n
∣m-n∣≤m⊔n zero    m       = ≤-refl
∣m-n∣≤m⊔n (suc m) zero    = ≤-refl
∣m-n∣≤m⊔n (suc m) (suc n) = ≤-step (∣m-n∣≤m⊔n m n)

∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
∣-∣-identityˡ x = refl

∣-∣-identityʳ : RightIdentity 0 ∣_-_∣
∣-∣-identityʳ zero    = refl
∣-∣-identityʳ (suc x) = refl

∣-∣-identity : Identity 0 ∣_-_∣
∣-∣-identity = ∣-∣-identityˡ , ∣-∣-identityʳ

∣-∣-comm : Commutative ∣_-_∣
∣-∣-comm zero    zero    = refl
∣-∣-comm zero    (suc n) = refl
∣-∣-comm (suc m) zero    = refl
∣-∣-comm (suc m) (suc n) = ∣-∣-comm m n

∣m-n∣≡[m∸n]∨[n∸m] : ∀ m n → (∣ m - n ∣ ≡ m ∸ n) ⊎ (∣ m - n ∣ ≡ n ∸ m)
∣m-n∣≡[m∸n]∨[n∸m] m n with ≤-total m n
... | inj₂ n≤m = inj₁ $ m≤n⇒∣n-m∣≡n∸m n≤m
... | inj₁ m≤n = inj₂ $ begin-equality
  ∣ m - n ∣ ≡⟨ ∣-∣-comm m n ⟩
  ∣ n - m ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m m≤n ⟩
  n ∸ m     ∎

private

  *-distribˡ-∣-∣-aux : ∀ a m n → m ≤ n → a * ∣ n - m ∣ ≡ ∣ a * n - a * m ∣
  *-distribˡ-∣-∣-aux a m n m≤n = begin-equality
    a * ∣ n - m ∣     ≡⟨ cong (a *_) (m≤n⇒∣n-m∣≡n∸m m≤n) ⟩
    a * (n ∸ m)       ≡⟨ *-distribˡ-∸ a n m ⟩
    a * n ∸ a * m     ≡⟨ sym $′ m≤n⇒∣n-m∣≡n∸m (*-monoʳ-≤ a m≤n) ⟩
    ∣ a * n - a * m ∣ ∎

*-distribˡ-∣-∣ : _*_ DistributesOverˡ ∣_-_∣
*-distribˡ-∣-∣ a m n with ≤-total m n
... | inj₂ n≤m = *-distribˡ-∣-∣-aux a n m n≤m
... | inj₁ m≤n = begin-equality
  a * ∣ m - n ∣     ≡⟨ cong (a *_) (∣-∣-comm m n) ⟩
  a * ∣ n - m ∣     ≡⟨ *-distribˡ-∣-∣-aux a m n m≤n ⟩
  ∣ a * n - a * m ∣ ≡⟨ ∣-∣-comm (a * n) (a * m) ⟩
  ∣ a * m - a * n ∣ ∎

*-distribʳ-∣-∣ : _*_ DistributesOverʳ ∣_-_∣
*-distribʳ-∣-∣ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-∣-∣

*-distrib-∣-∣ : _*_ DistributesOver ∣_-_∣
*-distrib-∣-∣ = *-distribˡ-∣-∣ , *-distribʳ-∣-∣

m≤n+∣n-m∣ : ∀ m n → m ≤ n + ∣ n - m ∣
m≤n+∣n-m∣ zero    n       = z≤n
m≤n+∣n-m∣ (suc m) zero    = ≤-refl
m≤n+∣n-m∣ (suc m) (suc n) = s≤s (m≤n+∣n-m∣ m n)

m≤n+∣m-n∣ : ∀ m n → m ≤ n + ∣ m - n ∣
m≤n+∣m-n∣ m n = subst (m ≤_) (cong (n +_) (∣-∣-comm n m)) (m≤n+∣n-m∣ m n)

m≤∣m-n∣+n : ∀ m n → m ≤ ∣ m - n ∣ + n
m≤∣m-n∣+n m n = subst (m ≤_) (+-comm n _) (m≤n+∣m-n∣ m n)

∣-∣-triangle : TriangleInequality ∣_-_∣
∣-∣-triangle zero    y       z       = m≤n+∣n-m∣ z y
∣-∣-triangle x       zero    z       = begin
  ∣ x - z ∣     ≤⟨ ∣m-n∣≤m⊔n x z ⟩
  x ⊔ z         ≤⟨ m⊔n≤m+n x z ⟩
  x + z         ≡⟨ cong₂ _+_ (sym (∣-∣-identityʳ x)) refl ⟩
  ∣ x - 0 ∣ + z ∎
  where open ≤-Reasoning
∣-∣-triangle x       y       zero    = begin
  ∣ x - 0 ∣             ≡⟨ ∣-∣-identityʳ x ⟩
  x                     ≤⟨ m≤∣m-n∣+n x y ⟩
  ∣ x - y ∣ + y         ≡⟨ cong₂ _+_ refl (sym (∣-∣-identityʳ y)) ⟩
  ∣ x - y ∣ + ∣ y - 0 ∣ ∎
  where open ≤-Reasoning
∣-∣-triangle (suc x) (suc y) (suc z) = ∣-∣-triangle x y z

------------------------------------------------------------------------
-- Metric structures

∣-∣-isProtoMetric : IsProtoMetric _≡_ ∣_-_∣
∣-∣-isProtoMetric = record
  { isPartialOrder  = ≤-isPartialOrder
  ; ≈-isEquivalence = isEquivalence
  ; cong            = cong₂ ∣_-_∣
  ; nonNegative     = z≤n
  }

∣-∣-isPreMetric : IsPreMetric _≡_ ∣_-_∣
∣-∣-isPreMetric = record
  { isProtoMetric = ∣-∣-isProtoMetric
  ; ≈⇒0           = m≡n⇒∣m-n∣≡0
  }

∣-∣-isQuasiSemiMetric : IsQuasiSemiMetric _≡_ ∣_-_∣
∣-∣-isQuasiSemiMetric = record
  { isPreMetric = ∣-∣-isPreMetric
  ; 0⇒≈         = ∣m-n∣≡0⇒m≡n
  }

∣-∣-isSemiMetric : IsSemiMetric _≡_ ∣_-_∣
∣-∣-isSemiMetric = record
  { isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
  ; sym               = ∣-∣-comm
  }

∣-∣-isMetric : IsMetric _≡_ ∣_-_∣
∣-∣-isMetric = record
  { isSemiMetric = ∣-∣-isSemiMetric
  ; triangle     = ∣-∣-triangle
  }

------------------------------------------------------------------------
-- Metric bundles

∣-∣-quasiSemiMetric : QuasiSemiMetric 0ℓ 0ℓ
∣-∣-quasiSemiMetric = record
  { isQuasiSemiMetric = ∣-∣-isQuasiSemiMetric
  }

∣-∣-semiMetric : SemiMetric 0ℓ 0ℓ
∣-∣-semiMetric = record
  { isSemiMetric = ∣-∣-isSemiMetric
  }

∣-∣-preMetric : PreMetric 0ℓ 0ℓ
∣-∣-preMetric = record
  { isPreMetric = ∣-∣-isPreMetric
  }

∣-∣-metric : Metric 0ℓ 0ℓ
∣-∣-metric = record
  { isMetric = ∣-∣-isMetric
  }

------------------------------------------------------------------------
-- Properties of ⌊_/2⌋ and ⌈_/2⌉
------------------------------------------------------------------------

⌊n/2⌋-mono : ⌊_/2⌋ Preserves _≤_ ⟶ _≤_
⌊n/2⌋-mono z≤n             = z≤n
⌊n/2⌋-mono (s≤s z≤n)       = z≤n
⌊n/2⌋-mono (s≤s (s≤s m≤n)) = s≤s (⌊n/2⌋-mono m≤n)

⌈n/2⌉-mono : ⌈_/2⌉ Preserves _≤_ ⟶ _≤_
⌈n/2⌉-mono m≤n = ⌊n/2⌋-mono (s≤s m≤n)

⌊n/2⌋≤⌈n/2⌉ : ∀ n → ⌊ n /2⌋ ≤ ⌈ n /2⌉
⌊n/2⌋≤⌈n/2⌉ zero          = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc zero)    = z≤n
⌊n/2⌋≤⌈n/2⌉ (suc (suc n)) = s≤s (⌊n/2⌋≤⌈n/2⌉ n)

⌊n/2⌋+⌈n/2⌉≡n : ∀ n → ⌊ n /2⌋ + ⌈ n /2⌉ ≡ n
⌊n/2⌋+⌈n/2⌉≡n zero    = refl
⌊n/2⌋+⌈n/2⌉≡n (suc n) = begin-equality
  ⌊ suc n /2⌋ + suc ⌊ n /2⌋   ≡⟨ +-comm ⌊ suc n /2⌋ (suc ⌊ n /2⌋) ⟩
  suc ⌊ n /2⌋ + ⌊ suc n /2⌋   ≡⟨⟩
  suc (⌊ n /2⌋ + ⌊ suc n /2⌋) ≡⟨ cong suc (⌊n/2⌋+⌈n/2⌉≡n n) ⟩
  suc n                       ∎

⌊n/2⌋≤n : ∀ n → ⌊ n /2⌋ ≤ n
⌊n/2⌋≤n zero          = z≤n
⌊n/2⌋≤n (suc zero)    = z≤n
⌊n/2⌋≤n (suc (suc n)) = s≤s (≤-step (⌊n/2⌋≤n n))

⌊n/2⌋<n : ∀ n → ⌊ suc n /2⌋ < suc n
⌊n/2⌋<n zero    = s≤s z≤n
⌊n/2⌋<n (suc n) = s≤s (s≤s (⌊n/2⌋≤n n))

⌈n/2⌉≤n : ∀ n → ⌈ n /2⌉ ≤ n
⌈n/2⌉≤n zero = z≤n
⌈n/2⌉≤n (suc n) = s≤s (⌊n/2⌋≤n n)

⌈n/2⌉<n : ∀ n → ⌈ suc (suc n) /2⌉ < suc (suc n)
⌈n/2⌉<n n = s≤s (⌊n/2⌋<n n)

------------------------------------------------------------------------
-- Properties of _≤′_ and _<′_
------------------------------------------------------------------------

≤′-trans : Transitive _≤′_
≤′-trans m≤n ≤′-refl       = m≤n
≤′-trans m≤n (≤′-step n≤o) = ≤′-step (≤′-trans m≤n n≤o)

z≤′n : ∀ {n} → zero ≤′ n
z≤′n {zero}  = ≤′-refl
z≤′n {suc n} = ≤′-step z≤′n

s≤′s : ∀ {m n} → m ≤′ n → suc m ≤′ suc n
s≤′s ≤′-refl        = ≤′-refl
s≤′s (≤′-step m≤′n) = ≤′-step (s≤′s m≤′n)

≤′⇒≤ : _≤′_ ⇒ _≤_
≤′⇒≤ ≤′-refl        = ≤-refl
≤′⇒≤ (≤′-step m≤′n) = ≤-step (≤′⇒≤ m≤′n)

≤⇒≤′ : _≤_ ⇒ _≤′_
≤⇒≤′ z≤n       = z≤′n
≤⇒≤′ (s≤s m≤n) = s≤′s (≤⇒≤′ m≤n)

≤′-step-injective : ∀ {m n} {p q : m ≤′ n} → ≤′-step p ≡ ≤′-step q → p ≡ q
≤′-step-injective refl = refl

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

_≤′?_ : Decidable _≤′_
m ≤′? n = map′ ≤⇒≤′ ≤′⇒≤ (m ≤? n)

_<′?_ : Decidable _<′_
m <′? n = suc m ≤′? n

_≥′?_ : Decidable _≥′_
_≥′?_ = flip _≤′?_

_>′?_ : Decidable _>′_
_>′?_ = flip _<′?_

m≤′m+n : ∀ m n → m ≤′ m + n
m≤′m+n m n = ≤⇒≤′ (m≤m+n m n)

n≤′m+n : ∀ m n → n ≤′ m + n
n≤′m+n zero    n = ≤′-refl
n≤′m+n (suc m) n = ≤′-step (n≤′m+n m n)

⌈n/2⌉≤′n : ∀ n → ⌈ n /2⌉ ≤′ n
⌈n/2⌉≤′n zero          = ≤′-refl
⌈n/2⌉≤′n (suc zero)    = ≤′-refl
⌈n/2⌉≤′n (suc (suc n)) = s≤′s (≤′-step (⌈n/2⌉≤′n n))

⌊n/2⌋≤′n : ∀ n → ⌊ n /2⌋ ≤′ n
⌊n/2⌋≤′n zero    = ≤′-refl
⌊n/2⌋≤′n (suc n) = ≤′-step (⌈n/2⌉≤′n n)

------------------------------------------------------------------------
-- Properties of _≤″_ and _<″_
------------------------------------------------------------------------

m<ᵇn⇒1+m+[n-1+m]≡n : ∀ m n → T (m <ᵇ n) → suc m + (n ∸ suc m) ≡ n
m<ᵇn⇒1+m+[n-1+m]≡n m n lt = m+[n∸m]≡n (<ᵇ⇒< m n lt)

m<ᵇ1+m+n : ∀ m {n} → T (m <ᵇ suc (m + n))
m<ᵇ1+m+n m = <⇒<ᵇ (m≤m+n (suc m) _)

<ᵇ⇒<″ : ∀ {m n} → T (m <ᵇ n) → m <″ n
<ᵇ⇒<″ {m} {n} leq = less-than-or-equal (m+[n∸m]≡n (<ᵇ⇒< m n leq))

<″⇒<ᵇ : ∀ {m n} → m <″ n → T (m <ᵇ n)
<″⇒<ᵇ {m} (less-than-or-equal refl) = <⇒<ᵇ (m≤m+n (suc m) _)

-- equivalence to _≤_

≤″⇒≤ : _≤″_ ⇒ _≤_
≤″⇒≤ {zero}  (less-than-or-equal refl) = z≤n
≤″⇒≤ {suc m} (less-than-or-equal refl) =
  s≤s (≤″⇒≤ (less-than-or-equal refl))

≤⇒≤″ : _≤_ ⇒ _≤″_
≤⇒≤″ = less-than-or-equal ∘ m+[n∸m]≡n

-- NB: we use the builtin function `_<ᵇ_ : (m n : ℕ) → Bool` here so
-- that the function quickly decides whether to return `yes` or `no`.
-- It still takes a linear amount of time to generate the proof if it
-- is inspected. We expect the main benefit to be visible for compiled
-- code: the backend erases proofs.

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

_<″?_ : Decidable _<″_
m <″? n = map′ <ᵇ⇒<″ <″⇒<ᵇ (T? (m <ᵇ n))

_≤″?_ : Decidable _≤″_
zero  ≤″? n = yes (less-than-or-equal refl)
suc m ≤″? n = m <″? n

_≥″?_ : Decidable _≥″_
_≥″?_ = flip _≤″?_

_>″?_ : Decidable _>″_
_>″?_ = flip _<″?_

≤″-irrelevant : Irrelevant _≤″_
≤″-irrelevant {m} (less-than-or-equal eq₁)
                  (less-than-or-equal eq₂)
  with +-cancelˡ-≡ m (trans eq₁ (sym eq₂))
... | refl = cong less-than-or-equal (≡-irrelevant eq₁ eq₂)

<″-irrelevant : Irrelevant _<″_
<″-irrelevant = ≤″-irrelevant

>″-irrelevant : Irrelevant _>″_
>″-irrelevant = ≤″-irrelevant

≥″-irrelevant : Irrelevant _≥″_
≥″-irrelevant = ≤″-irrelevant

------------------------------------------------------------------------
-- Properties of _≤‴_
------------------------------------------------------------------------

≤‴⇒≤″ : ∀{m n} → m ≤‴ n → m ≤″ n
≤‴⇒≤″ {m = m} ≤‴-refl     = less-than-or-equal {k = 0} (+-identityʳ m)
≤‴⇒≤″ {m = m} (≤‴-step x) = less-than-or-equal (trans (+-suc m _) (_≤″_.proof ind)) where
  ind = ≤‴⇒≤″ x

m≤‴m+k : ∀{m n k} → m + k ≡ n → m ≤‴ n
m≤‴m+k {m} {k = zero} refl = subst (λ z → m ≤‴ z) (sym (+-identityʳ m)) (≤‴-refl {m})
m≤‴m+k {m} {k = suc k} proof
  = ≤‴-step (m≤‴m+k {k = k} (trans (sym (+-suc m _)) proof))

≤″⇒≤‴ : ∀{m n} → m ≤″ n → m ≤‴ n
≤″⇒≤‴ (less-than-or-equal {k} proof) = m≤‴m+k proof

0≤‴n : ∀{n} → 0 ≤‴ n
0≤‴n {n} = m≤‴m+k refl

<ᵇ⇒<‴ : ∀ {m n} → T (m <ᵇ n) → m <‴ n
<ᵇ⇒<‴ {m} {n} leq = ≤″⇒≤‴ (<ᵇ⇒<″ leq)

<‴⇒<ᵇ : ∀ {m n} → m <‴ n → T (m <ᵇ n)
<‴⇒<ᵇ leq = <″⇒<ᵇ (≤‴⇒≤″ leq)

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

_<‴?_ : Decidable _<‴_
m <‴? n = map′ <ᵇ⇒<‴ <‴⇒<ᵇ (T? (m <ᵇ n))

_≤‴?_ : Decidable _≤‴_
zero ≤‴? n = yes 0≤‴n
suc m ≤‴? n = m <‴? n

_≥‴?_ : Decidable _≥‴_
_≥‴?_ = flip _≤‴?_

_>‴?_ : Decidable _>‴_
_>‴?_ = flip _<‴?_

≤⇒≤‴ : _≤_ ⇒ _≤‴_
≤⇒≤‴ = ≤″⇒≤‴ ∘ ≤⇒≤″

≤‴⇒≤ : _≤‴_ ⇒ _≤_
≤‴⇒≤ = ≤″⇒≤ ∘ ≤‴⇒≤″

------------------------------------------------------------------------
-- Other properties
------------------------------------------------------------------------

-- If there is an injection from a type to ℕ, then the type has
-- decidable equality.

eq? : ∀ {a} {A : Set a} → A ↣ ℕ → Decidable {A = A} _≡_
eq? inj = via-injection inj _≟_


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

-- Version 0.14

_*-mono_ = *-mono-≤
{-# WARNING_ON_USAGE _*-mono_
"Warning: _*-mono_ was deprecated in v0.14.
Please use *-mono-≤ instead."
#-}
_+-mono_ = +-mono-≤
{-# WARNING_ON_USAGE _+-mono_
"Warning: _+-mono_ was deprecated in v0.14.
Please use +-mono-≤ instead."
#-}
+-right-identity = +-identityʳ
{-# WARNING_ON_USAGE +-right-identity
"Warning: +-right-identity was deprecated in v0.14.
Please use +-identityʳ instead."
#-}
*-right-zero     = *-zeroʳ
{-# WARNING_ON_USAGE *-right-zero
"Warning: *-right-zero was deprecated in v0.14.
Please use *-zeroʳ instead."
#-}
distribʳ-*-+     = *-distribʳ-+
{-# WARNING_ON_USAGE distribʳ-*-+
"Warning: distribʳ-*-+ was deprecated in v0.14.
Please use *-distribʳ-+ instead."
#-}
*-distrib-∸ʳ     = *-distribʳ-∸
{-# WARNING_ON_USAGE *-distrib-∸ʳ
"Warning: *-distrib-∸ʳ was deprecated in v0.14.
Please use *-distribʳ-∸ instead."
#-}
cancel-+-left    = +-cancelˡ-≡
{-# WARNING_ON_USAGE cancel-+-left
"Warning: cancel-+-left was deprecated in v0.14.
Please use +-cancelˡ-≡ instead."
#-}
cancel-+-left-≤  = +-cancelˡ-≤
{-# WARNING_ON_USAGE cancel-+-left-≤
"Warning: cancel-+-left-≤ was deprecated in v0.14.
Please use +-cancelˡ-≤ instead."
#-}
cancel-*-right   = *-cancelʳ-≡
{-# WARNING_ON_USAGE cancel-*-right
"Warning: cancel-*-right was deprecated in v0.14.
Please use *-cancelʳ-≡ instead."
#-}
cancel-*-right-≤ = *-cancelʳ-≤
{-# WARNING_ON_USAGE cancel-*-right-≤
"Warning: cancel-*-right-≤ was deprecated in v0.14.
Please use *-cancelʳ-≤ instead."
#-}
strictTotalOrder                      = <-strictTotalOrder
{-# WARNING_ON_USAGE strictTotalOrder
"Warning: strictTotalOrder was deprecated in v0.14.
Please use <-strictTotalOrder instead."
#-}
isCommutativeSemiring                 = +-*-isCommutativeSemiring
{-# WARNING_ON_USAGE isCommutativeSemiring
"Warning: isCommutativeSemiring was deprecated in v0.14.
Please use *-+-isCommutativeSemiring instead."
#-}
commutativeSemiring                   = +-*-commutativeSemiring
{-# WARNING_ON_USAGE commutativeSemiring
"Warning: commutativeSemiring was deprecated in v0.14.
Please use *-+-commutativeSemiring instead."
#-}
isDistributiveLattice                 = ⊓-⊔-isDistributiveLattice
{-# WARNING_ON_USAGE isDistributiveLattice
"Warning: isDistributiveLattice was deprecated in v0.14.
Please use ⊓-⊔-isDistributiveLattice instead."
#-}
distributiveLattice                   = ⊓-⊔-distributiveLattice
{-# WARNING_ON_USAGE distributiveLattice
"Warning: distributiveLattice was deprecated in v0.14.
Please use ⊓-⊔-distributiveLattice instead."
#-}
⊔-⊓-0-isSemiringWithoutOne            = ⊔-⊓-isSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-isSemiringWithoutOne
"Warning: ⊔-⊓-0-isSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-isSemiringWithoutOne instead."
#-}
⊔-⊓-0-isCommutativeSemiringWithoutOne = ⊔-⊓-isCommutativeSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-isCommutativeSemiringWithoutOne
"Warning: ⊔-⊓-0-isCommutativeSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-isCommutativeSemiringWithoutOne instead."
#-}
⊔-⊓-0-commutativeSemiringWithoutOne   = ⊔-⊓-commutativeSemiringWithoutOne
{-# WARNING_ON_USAGE ⊔-⊓-0-commutativeSemiringWithoutOne
"Warning: ⊔-⊓-0-commutativeSemiringWithoutOne was deprecated in v0.14.
Please use ⊔-⊓-commutativeSemiringWithoutOne instead."
#-}

-- Version 0.15

¬i+1+j≤i  = m+1+n≰m
{-# WARNING_ON_USAGE ¬i+1+j≤i
"Warning: ¬i+1+j≤i was deprecated in v0.15.
Please use m+1+n≰m instead."
#-}
≤-steps   = ≤-stepsˡ
{-# WARNING_ON_USAGE ≤-steps
"Warning: ≤-steps was deprecated in v0.15.
Please use ≤-stepsˡ instead."
#-}

-- Version 0.17

i∸k∸j+j∸k≡i+j∸k : ∀ i j k → i ∸ (k ∸ j) + (j ∸ k) ≡ i + j ∸ k
i∸k∸j+j∸k≡i+j∸k zero    j k    = cong (_+ (j ∸ k)) (0∸n≡0 (k ∸ j))
i∸k∸j+j∸k≡i+j∸k (suc i) j zero = cong (λ x → suc i ∸ x + j) (0∸n≡0 j)
i∸k∸j+j∸k≡i+j∸k (suc i) zero (suc k) = begin-equality
  i ∸ k + 0  ≡⟨ +-identityʳ _ ⟩
  i ∸ k      ≡⟨ cong (_∸ k) (sym (+-identityʳ _)) ⟩
  i + 0 ∸ k  ∎
i∸k∸j+j∸k≡i+j∸k (suc i) (suc j) (suc k) = begin-equality
  suc i ∸ (k ∸ j) + (j ∸ k) ≡⟨ i∸k∸j+j∸k≡i+j∸k (suc i) j k ⟩
  suc i + j ∸ k             ≡⟨ cong (_∸ k) (sym (+-suc i j)) ⟩
  i + suc j ∸ k             ∎
{-# WARNING_ON_USAGE i∸k∸j+j∸k≡i+j∸k
"Warning: i∸k∸j+j∸k≡i+j∸k was deprecated in v0.17."
#-}
im≡jm+n⇒[i∸j]m≡n : ∀ i j m n → i * m ≡ j * m + n → (i ∸ j) * m ≡ n
im≡jm+n⇒[i∸j]m≡n i j m n eq = begin-equality
  (i ∸ j) * m            ≡⟨ *-distribʳ-∸ m i j ⟩
  (i * m) ∸ (j * m)      ≡⟨ cong (_∸ j * m) eq ⟩
  (j * m + n) ∸ (j * m)  ≡⟨ cong (_∸ j * m) (+-comm (j * m) n) ⟩
  (n + j * m) ∸ (j * m)  ≡⟨ m+n∸n≡m n (j * m) ⟩
  n                      ∎
{-# WARNING_ON_USAGE im≡jm+n⇒[i∸j]m≡n
"Warning: im≡jm+n⇒[i∸j]m≡n was deprecated in v0.17."
#-}
≤+≢⇒< = ≤∧≢⇒<
{-# WARNING_ON_USAGE ≤+≢⇒<
"Warning: ≤+≢⇒< was deprecated in v0.17.
Please use ≤∧≢⇒< instead."
#-}

-- Version 1.0

≤-irrelevance = ≤-irrelevant
{-# WARNING_ON_USAGE ≤-irrelevance
"Warning: ≤-irrelevance was deprecated in v1.0.
Please use ≤-irrelevant instead."
#-}
<-irrelevance = <-irrelevant
{-# WARNING_ON_USAGE <-irrelevance
"Warning: <-irrelevance was deprecated in v1.0.
Please use <-irrelevant instead."
#-}

-- Version 1.1

i+1+j≢i = m+1+n≢m
{-# WARNING_ON_USAGE i+1+j≢i
"Warning: i+1+j≢i was deprecated in v1.1.
Please use m+1+n≢m instead."
#-}
i+j≡0⇒i≡0 = m+n≡0⇒m≡0
{-# WARNING_ON_USAGE i+j≡0⇒i≡0
"Warning: i+j≡0⇒i≡0 was deprecated in v1.1.
Please use m+n≡0⇒m≡0 instead."
#-}
i+j≡0⇒j≡0 = m+n≡0⇒n≡0
{-# WARNING_ON_USAGE i+j≡0⇒j≡0
"Warning: i+j≡0⇒j≡0 was deprecated in v1.1.
Please use m+n≡0⇒n≡0 instead."
#-}
i+1+j≰i = m+1+n≰m
{-# WARNING_ON_USAGE i+1+j≰i
"Warning: i+1+j≰i was deprecated in v1.1.
Please use m+1+n≰m instead."
#-}
i*j≡0⇒i≡0∨j≡0 = m*n≡0⇒m≡0∨n≡0
{-# WARNING_ON_USAGE i*j≡0⇒i≡0∨j≡0
"Warning: i*j≡0⇒i≡0∨j≡0 was deprecated in v1.1.
Please use m*n≡0⇒m≡0∨n≡0 instead."
#-}
i*j≡1⇒i≡1 = m*n≡1⇒m≡1
{-# WARNING_ON_USAGE i*j≡1⇒i≡1
"Warning: i*j≡1⇒i≡1 was deprecated in v1.1.
Please use m*n≡1⇒m≡1 instead."
#-}
i*j≡1⇒j≡1 = m*n≡1⇒n≡1
{-# WARNING_ON_USAGE i*j≡1⇒j≡1
"Warning: i*j≡1⇒j≡1 was deprecated in v1.1.
Please use m*n≡1⇒n≡1 instead."
#-}
i^j≡0⇒i≡0 = m^n≡0⇒m≡0
{-# WARNING_ON_USAGE i^j≡0⇒i≡0
"Warning: i^j≡0⇒i≡0 was deprecated in v1.1.
Please use m^n≡0⇒m≡0 instead."
#-}
i^j≡1⇒j≡0∨i≡1 = m^n≡1⇒n≡0∨m≡1
{-# WARNING_ON_USAGE i^j≡1⇒j≡0∨i≡1
"Warning: i^j≡1⇒j≡0∨i≡1 was deprecated in v1.1.
Please use m^n≡1⇒n≡0∨m≡1 instead."
#-}
[i+j]∸[i+k]≡j∸k = [m+n]∸[m+o]≡n∸o
{-# WARNING_ON_USAGE [i+j]∸[i+k]≡j∸k
"Warning: [i+j]∸[i+k]≡j∸k was deprecated in v1.1.
Please use [m+n]∸[m+o]≡n∸o instead."
#-}
m≢0⇒suc[pred[m]]≡m = suc[pred[n]]≡n
{-# WARNING_ON_USAGE m≢0⇒suc[pred[m]]≡m
"Warning: m≢0⇒suc[pred[m]]≡m was deprecated in v1.1.
Please use suc[pred[n]]≡n instead."
#-}
n≡m⇒∣n-m∣≡0 = m≡n⇒∣m-n∣≡0
{-# WARNING_ON_USAGE n≡m⇒∣n-m∣≡0
"Warning: n≡m⇒∣n-m∣≡0 was deprecated in v1.1.
Please use m≡n⇒∣m-n∣≡0 instead."
#-}
∣n-m∣≡0⇒n≡m = ∣m-n∣≡0⇒m≡n
{-# WARNING_ON_USAGE ∣n-m∣≡0⇒n≡m
"Warning: ∣n-m∣≡0⇒n≡m was deprecated in v1.1.
Please use ∣m-n∣≡0⇒m≡n instead."
#-}
∣n-m∣≡n∸m⇒m≤n = ∣m-n∣≡m∸n⇒n≤m
{-# WARNING_ON_USAGE ∣n-m∣≡n∸m⇒m≤n
"Warning: ∣n-m∣≡n∸m⇒m≤n was deprecated in v1.1.
Please use ∣m-n∣≡m∸n⇒n≤m instead."
#-}
∣n-n+m∣≡m = ∣m-m+n∣≡n
{-# WARNING_ON_USAGE ∣n-n+m∣≡m
"Warning: ∣n-n+m∣≡m was deprecated in v1.1.
Please use ∣m-m+n∣≡n instead."
#-}
∣n+m-n+o∣≡∣m-o| = ∣m+n-m+o∣≡∣n-o|
{-# WARNING_ON_USAGE ∣n+m-n+o∣≡∣m-o|
"Warning: ∣n+m-n+o∣≡∣m-o| was deprecated in v1.1.
Please use ∣m+n-m+o∣≡∣n-o| instead."
#-}
n∸m≤∣n-m∣ = m∸n≤∣m-n∣
{-# WARNING_ON_USAGE n∸m≤∣n-m∣
"Warning: n∸m≤∣n-m∣ was deprecated in v1.1.
Please use m∸n≤∣m-n∣ instead."
#-}
∣n-m∣≤n⊔m = ∣m-n∣≤m⊔n
{-# WARNING_ON_USAGE ∣n-m∣≤n⊔m
"Warning: ∣n-m∣≤n⊔m was deprecated in v1.1.
Please use ∣m-n∣≤m⊔n instead."
#-}
n≤m+n : ∀ m n → n ≤ m + n
n≤m+n m n = subst (n ≤_) (+-comm n m) (m≤m+n n m)
{-# WARNING_ON_USAGE n≤m+n
"Warning: n≤m+n was deprecated in v1.1.
Please use m≤n+m instead (note, you will need to switch the argument order)."
#-}
n≤m+n∸m : ∀ m n → n ≤ m + (n ∸ m)
n≤m+n∸m m       zero    = z≤n
n≤m+n∸m zero    (suc n) = ≤-refl
n≤m+n∸m (suc m) (suc n) = s≤s (n≤m+n∸m m n)
{-# WARNING_ON_USAGE n≤m+n∸m
"Warning: n≤m+n∸m was deprecated in v1.1.
Please use m≤n+m∸n instead (note, you will need to switch the argument order)."
#-}
∣n-m∣≡[n∸m]∨[m∸n] : ∀ m n → (∣ n - m ∣ ≡ n ∸ m) ⊎ (∣ n - m ∣ ≡ m ∸ n)
∣n-m∣≡[n∸m]∨[m∸n] m n with ≤-total m n
... | inj₁ m≤n = inj₁ $ m≤n⇒∣n-m∣≡n∸m m≤n
... | inj₂ n≤m = inj₂ $ begin-equality
  ∣ n - m ∣ ≡⟨ ∣-∣-comm n m ⟩
  ∣ m - n ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m n≤m ⟩
  m ∸ n     ∎
{-# WARNING_ON_USAGE ∣n-m∣≡[n∸m]∨[m∸n]
"Warning: ∣n-m∣≡[n∸m]∨[m∸n] was deprecated in v1.1.
Please use ∣m-n∣≡[m∸n]∨[n∸m] instead (note, you will need to switch the argument order)."
#-}

-- Version 1.2

+-*-suc = *-suc
{-# WARNING_ON_USAGE +-*-suc
"Warning: +-*-suc was deprecated in v1.2.
Please use *-suc instead."
#-}

n∸m≤n : ∀ m n → n ∸ m ≤ n
n∸m≤n m n = m∸n≤m n m
{-# WARNING_ON_USAGE n∸m≤n
"Warning: n∸m≤n was deprecated in v1.2.
Please use m∸n≤m instead (note, you will need to switch the argument order)."
#-}

-- Version 1.3

∀[m≤n⇒m≢o]⇒o<n : ∀ n o → (∀ {m} → m ≤ n → m ≢ o) → n < o
∀[m≤n⇒m≢o]⇒o<n = ∀[m≤n⇒m≢o]⇒n<o
{-# WARNING_ON_USAGE ∀[m≤n⇒m≢o]⇒o<n
"Warning: ∀[m≤n⇒m≢o]⇒o<n was deprecated in v1.3.
Please use ∀[m≤n⇒m≢o]⇒n<o instead."
#-}
∀[m<n⇒m≢o]⇒o≤n : ∀ n o → (∀ {m} → m < n → m ≢ o) → n ≤ o
∀[m<n⇒m≢o]⇒o≤n = ∀[m<n⇒m≢o]⇒n≤o
{-# WARNING_ON_USAGE ∀[m<n⇒m≢o]⇒o≤n
"Warning: ∀[m<n⇒m≢o]⇒o≤n was deprecated in v1.3.
Please use ∀[m<n⇒m≢o]⇒n≤o instead."
#-}

-- Version 1.4

*-+-isSemiring = +-*-isSemiring
{-# WARNING_ON_USAGE *-+-isSemiring
"Warning: *-+-isSemiring was deprecated in v1.4.
Please use +-*-isSemiring instead."
#-}
*-+-isCommutativeSemiring = +-*-isCommutativeSemiring
{-# WARNING_ON_USAGE *-+-isCommutativeSemiring
"Warning: *-+-isCommutativeSemiring was deprecated in v1.4.
Please use +-*-isCommutativeSemiring instead."
#-}
*-+-semiring = +-*-semiring
{-# WARNING_ON_USAGE *-+-semiring
"Warning: *-+-semiring was deprecated in v1.4.
Please use +-*-semiring instead."
#-}
*-+-commutativeSemiring = +-*-commutativeSemiring
{-# WARNING_ON_USAGE *-+-commutativeSemiring
"Warning: *-+-commutativeSemiring was deprecated in v1.4.
Please use +-*-commutativeSemiring instead."
#-}