diff --git a/CHANGELOG.md b/CHANGELOG.md
index b025b64de8..7db05f126f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -156,6 +156,13 @@ New modules
 
 * `Effect.Foldable`: implementation of haskell-like `Foldable`
 
+* Integer arithmetic modulo `n`, based on `Data.Nat.Bounded.*`:
+  ```agda
+  Data.Integer.Modulo.Base
+  Data.Integer.Modulo.Literals
+  Data.Integer.Modulo.Properties
+  ```
+
 Additions to existing modules
 -----------------------------
 
diff --git a/src/Data/Integer/Modulo/Base.agda b/src/Data/Integer/Modulo/Base.agda
new file mode 100644
index 0000000000..0cef16ca1c
--- /dev/null
+++ b/src/Data/Integer/Modulo/Base.agda
@@ -0,0 +1,118 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Integers mod n, type and basic operations
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Data.Nat.Base as ℕ
+  using (ℕ; zero; suc; NonZero; NonTrivial; nonTrivial⇒nonZero; _<_; _∸_)
+
+module Data.Integer.Modulo.Base n .{{_ : NonTrivial n}} where
+
+open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing)
+open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs)
+open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_; ≡-Modℕ)
+import Data.Nat.Properties as ℕ
+open import Data.Sign.Base as Sign using (Sign)
+open import Data.Unit.Base using (⊤)
+open import Function.Base using (id; _∘_; _$_; _on_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+
+private
+  variable
+    m o : ℕ
+    i j : ℕ< n
+
+  instance
+    _ = nonTrivial⇒nonZero n
+
+  m∸n<m : ∀ m n → .{{NonZero m}} → .{{NonZero n}} → m ∸ n < m
+  m∸n<m m@(suc _) n@(suc o) = ℕ.s≤s (ℕ.m∸n≤m _ o)
+
+------------------------------------------------------------------------
+-- Definition
+
+-- Infixes
+infix  8 -_
+infixl 7 _*_
+infixl 6 _+_
+
+-- Type definition
+ℤmod : Set
+ℤmod = ℕ< n
+
+-- Re-export
+fromℕ : ℕ → ℤmod
+fromℕ = ℕ<.fromℕ
+
+-- Negation
+-_ : ℤmod → ℤmod
+- ⟦ m@zero ⟧< _    = ⟦0⟧<
+- ⟦ m@(suc _) ⟧< _ = ⟦ n ∸ m ⟧< m∸n<m _ _
+
+-- Addition
+_+_ : ℤmod → ℤmod → ℤmod
+i + j = fromℕ (⟦ i ⟧ ℕ.+ ⟦ j ⟧)
+
+-- Multiplication
+_*_ : ℤmod → ℤmod → ℤmod
+i * j = fromℕ (⟦ i ⟧ ℕ.* ⟦ j ⟧)
+
+------------------------------------------------------------------------
+-- Quotient map from ℤ
+
+_◃_ : Sign → ℤmod → ℤmod
+Sign.+ ◃ j = j
+Sign.- ◃ j = - j
+
+fromℤ : ℤ → ℤmod
+fromℤ i with s ◂ ∣i∣ ← signAbs i = s ◃ fromℕ ∣i∣
+
+-- the _mod_ syntax
+
+Mod : ℤ → ℤmod
+Mod = fromℤ
+
+syntax Mod {n = n} i = i mod n
+
+-- Quotient equivalence relation on ℤ induced by `fromℤ`
+
+_∼_ : Rel ℤ _
+_∼_ = _≡_ on fromℤ
+
+≡-Mod : Rel ℤ _
+≡-Mod i j = i ∼ j
+
+syntax ≡-Mod n i j = i ≡ j mod n
+
+------------------------------------------------------------------------
+-- Raw bundles
+
++-*-rawRing : RawRing _ _
++-*-rawRing = record
+  { _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; -_ = -_
+  ; 0# = ⟦0⟧<
+  ; 1# = ⟦1⟧<
+  }
+
+open RawRing +-*-rawRing public
+  using (+-rawMagma; *-rawMagma)
+  renaming ( +-rawMonoid to +-0-rawMonoid
+           ; *-rawMonoid to *-1-rawMonoid
+           --; rawNearSemiring to +-*-rawNearSemiring
+           ; rawSemiring to +-*-rawSemiring
+           )
+
+------------------------------------------------------------------------
+-- -- Postfix notation for when opening the module unparameterised
+
+0ℤmod = ⟦0⟧<
+1ℤmod = ⟦1⟧<
+
diff --git a/src/Data/Integer/Modulo/Literals.agda b/src/Data/Integer/Modulo/Literals.agda
new file mode 100644
index 0000000000..481fe9e2e5
--- /dev/null
+++ b/src/Data/Integer/Modulo/Literals.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Literals for integers mod n
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Data.Nat.Base using (ℕ; NonTrivial)
+
+module Data.Integer.Modulo.Literals n .{{_ : NonTrivial n}} where
+
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Unit.Base using (⊤)
+open import Data.Integer.Modulo.Base using (ℤmod; fromℕ)
+
+------------------------------------------------------------------------
+-- Definitions
+
+Constraint : ℕ → Set
+Constraint _ = ⊤
+
+fromNat : ∀ m → {{Constraint m}} → ℤmod n
+fromNat m = fromℕ n m
+
+number : Number (ℤmod n)
+number = record { Constraint = Constraint ; fromNat = fromNat }
diff --git a/src/Data/Integer/Modulo/Properties.agda b/src/Data/Integer/Modulo/Properties.agda
new file mode 100644
index 0000000000..5dc33eebc4
--- /dev/null
+++ b/src/Data/Integer/Modulo/Properties.agda
@@ -0,0 +1,178 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Integers mod n, properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Data.Nat.Base as ℕ
+  using (ℕ; zero; suc; NonZero; NonTrivial; _<_; _∸_; _%_)
+
+module Data.Integer.Modulo.Properties n .{{_ : NonTrivial n}} where
+
+open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing)
+open import Algebra.Bundles
+  using (Magma; Monoid; NearSemiring; Semiring; Ring)
+import Algebra.Definitions as Definitions
+import Algebra.Structures as Structures
+open import Data.Integer.Base as ℤ using (ℤ; _◂_; signAbs)
+open import Data.Nat.Bounded.Base as ℕ< hiding (fromℕ; _∼_)
+import Data.Nat.Bounded.Properties as ℕ<
+import Data.Nat.DivMod as ℕ
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base as Product using (_,_)
+open import Data.Sign.Base as Sign using (Sign)
+open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; cong₂; isEquivalence; module ≡-Reasoning)
+
+open import Data.Integer.Modulo.Base n as Modulo
+  using (ℤmod; fromℕ; fromℤ; _∼_; ≡-Mod; +-*-rawRing)
+
+open Definitions (_≡_ {A = ℤmod})
+open Structures (_≡_ {A = ℤmod})
+  using ( IsMagma; IsSemigroup; IsMonoid
+        ; IsGroup; IsAbelianGroup
+        ; IsNearSemiring; IsSemiring
+        ; IsRing)
+
+private
+  variable
+    m o : ℕ
+    i j k : ℤmod
+
+  instance
+    _ = ℕ.nonTrivial⇒nonZero n
+
+open RawRing +-*-rawRing
+open ≡-Reasoning
+
++-cong₂ : Congruent₂ _+_
++-cong₂ = cong₂ _+_
+
++-isMagma : IsMagma _+_
++-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = +-cong₂ }
+
++-assoc : Associative _+_
++-assoc i j k = begin
+  i + j + k
+   ≡⟨⟩
+  fromℕ (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) % n) ℕ.+ ⟦ k ⟧)
+   ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩
+  fromℕ (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) % n))
+   ≡⟨⟩
+  i + (j + k) ∎
+  where
+  ≡-mod : (((⟦ i ⟧ ℕ.+ ⟦ j ⟧) % n) ℕ.+ ⟦ k ⟧)
+          ≡
+          (⟦ i ⟧ ℕ.+ ((⟦ j ⟧ ℕ.+ ⟦ k ⟧) % n))
+          modℕ n
+  ≡-mod = ℕ<.≡-mod-trans (ℕ<.+-distribˡ-% (⟦ i ⟧ ℕ.+ ⟦ j ⟧) ⟦ k ⟧)
+          (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.+-assoc ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧))
+           (ℕ<.≡-mod-sym (ℕ<.+-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.+ ⟦ k ⟧))))
+
++-isSemigroup : IsSemigroup _+_
++-isSemigroup = record { isMagma = +-isMagma ; assoc = +-assoc }
+
++-identityˡ : LeftIdentity 0# _+_
++-identityˡ = ℕ<.fromℕ∘toℕ≐id
+
++-identityʳ : RightIdentity 0# _+_
++-identityʳ i = trans (cong fromℕ (ℕ.+-identityʳ _)) (ℕ<.fromℕ∘toℕ≐id i)
+
++-identity : Identity 0# _+_
++-identity = +-identityˡ , +-identityʳ
+
++-isMonoid : IsMonoid _+_ 0#
++-isMonoid = record { isSemigroup = +-isSemigroup ; identity = +-identity }
+
++-inverseˡ : LeftInverse 0# -_ _+_
++-inverseˡ (⟦ zero ⟧<    _) = +-identityˡ 0#
++-inverseˡ i@(⟦ suc _ ⟧< _) = ℕ<.+-inverseˡ (ℕ<.isBounded i)
+
++-inverseʳ : RightInverse 0# -_ _+_
++-inverseʳ (⟦ zero ⟧<        _) = +-identityʳ 0#
++-inverseʳ i@(⟦ m@(suc _) ⟧< _) = ℕ<.+-inverseʳ (ℕ<.isBounded i)
+
++-inverse : Inverse 0# -_ _+_
++-inverse = +-inverseˡ , +-inverseʳ
+
++-0-isGroup : IsGroup _+_ 0# -_
++-0-isGroup = record { isMonoid = +-isMonoid ; inverse = +-inverse ; ⁻¹-cong = cong -_ }
+
++-comm : Commutative _+_
++-comm i j = cong fromℕ (ℕ.+-comm ⟦ i ⟧ ⟦ j ⟧)
+
++-0-isAbelianGroup : IsAbelianGroup _+_ 0# -_
++-0-isAbelianGroup = record { isGroup = +-0-isGroup ; comm = +-comm }
+
+*-cong₂ : Congruent₂ _*_
+*-cong₂ = cong₂ _*_
+
+*-assoc : Associative _*_
+*-assoc i j k = begin
+  i * j * k
+   ≡⟨⟩
+  fromℕ (((⟦ i ⟧ ℕ.* ⟦ j ⟧) % n) ℕ.* ⟦ k ⟧)
+   ≡⟨ ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod ⟩
+  fromℕ (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) % n))
+   ≡⟨⟩
+  i * (j * k) ∎
+  where
+  ≡-mod : (((⟦ i ⟧ ℕ.* ⟦ j ⟧) % n) ℕ.* ⟦ k ⟧)
+          ≡
+          (⟦ i ⟧ ℕ.* ((⟦ j ⟧ ℕ.* ⟦ k ⟧) % n))
+          modℕ n
+  ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribˡ-% (⟦ i ⟧ ℕ.* ⟦ j ⟧) ⟦ k ⟧)
+          (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-assoc ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧))
+           (ℕ<.≡-mod-sym (ℕ<.*-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.* ⟦ k ⟧))))
+
+*-identityˡ : LeftIdentity 1# _*_
+*-identityˡ i with eq ← ℕ<.⟦1⟧≡1 {n = n} rewrite eq
+  = trans (cong fromℕ (ℕ.*-identityˡ _)) (ℕ<.fromℕ≐⟦⟧< (ℕ<.isBounded i))
+
+*-identityʳ : RightIdentity 1# _*_
+*-identityʳ i with eq ← ℕ<.⟦1⟧≡1 {n = n} rewrite eq
+  = trans (cong fromℕ (ℕ.*-identityʳ _)) (ℕ<.fromℕ≐⟦⟧< (ℕ<.isBounded i))
+
+*-identity : Identity 1# _*_
+*-identity = *-identityˡ , *-identityʳ
+
+*-distribˡ-+ : _*_ DistributesOverˡ _+_
+*-distribˡ-+ i j k = ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod
+  where
+  ≡-mod : (⟦ i ⟧ ℕ.* ⟦ j + k ⟧)
+          ≡
+          (⟦ i * j ⟧ ℕ.+ ⟦ i * k ⟧)
+          modℕ n
+  ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribʳ-% ⟦ i ⟧ (⟦ j ⟧ ℕ.+ ⟦ k ⟧))
+          (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-distribˡ-+ ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧))
+           (ℕ<.≡-mod-sym (ℕ<.+-distrib-% (⟦ i ⟧ ℕ.* ⟦ j ⟧) (⟦ i ⟧ ℕ.* ⟦ k ⟧))))
+
+*-distribʳ-+ : _*_ DistributesOverʳ _+_
+*-distribʳ-+ i j k = ℕ<.≡-mod⇒fromℕ≡fromℕ ≡-mod
+  where
+  ≡-mod : (⟦ j + k ⟧ ℕ.* ⟦ i ⟧)
+          ≡
+          (⟦ j * i ⟧ ℕ.+ ⟦ k * i ⟧)
+          modℕ n
+  ≡-mod = ℕ<.≡-mod-trans (ℕ<.*-distribˡ-% (⟦ j ⟧ ℕ.+ ⟦ k ⟧) ⟦ i ⟧)
+          (ℕ<.≡-mod-trans (ℕ<.≡-mod-reflexive (ℕ.*-distribʳ-+ ⟦ i ⟧ ⟦ j ⟧ ⟦ k ⟧))
+           (ℕ<.≡-mod-sym (ℕ<.+-distrib-% (⟦ j ⟧ ℕ.* ⟦ i ⟧) (⟦ k ⟧ ℕ.* ⟦ i ⟧))))
+
+*-distrib-+ : _*_ DistributesOver _+_
+*-distrib-+ = *-distribˡ-+ , *-distribʳ-+
+
++-*-isRing : IsRing _+_ _*_ -_ 0# 1#
++-*-isRing = record
+  { +-isAbelianGroup = +-0-isAbelianGroup
+  ; *-cong           = *-cong₂
+  ; *-assoc          = *-assoc
+  ; *-identity       = *-identity
+  ; distrib          = *-distrib-+
+  }
+
+ring : Ring _ _
+ring = record { isRing = +-*-isRing }
diff --git a/src/Data/Nat/Bounded/Base.agda b/src/Data/Nat/Bounded/Base.agda
new file mode 100644
index 0000000000..a230b09b06
--- /dev/null
+++ b/src/Data/Nat/Bounded/Base.agda
@@ -0,0 +1,96 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Bounded natural numbers, and their equivalence to `Fin`
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Bounded.Base where
+
+open import Data.Nat.Base as ℕ
+import Data.Nat.DivMod as ℕ
+import Data.Nat.Properties as ℕ
+open import Data.Fin.Base as Fin using (Fin)
+import Data.Fin.Properties as Fin
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions
+open import Relation.Nullary.Decidable.Core using (recompute)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+private
+  variable
+    m n o : ℕ
+
+------------------------------------------------------------------------
+-- Definition
+
+record ℕ< (n : ℕ) : Set where
+  constructor ⟦_⟧<_
+  field
+    ⟦_⟧ : ℕ
+    .bounded : ⟦_⟧ < n
+
+open ℕ< public using (⟦_⟧)
+
+-- Constructors: 'n-1 mod n', '0 mod n', '1 mod n'
+
+⟦-1⟧< ⟦0⟧< ⟦1⟧< : .{{ NonZero n }} → ℕ< n
+⟦-1⟧< {n = suc m} = ⟦ m ⟧< ℕ.n<1+n m
+⟦0⟧<              = ⟦ 0 ⟧< >-nonZero⁻¹ _
+⟦1⟧<  {n = 1}     = ⟦0⟧<
+⟦1⟧<  {n = 2+ _}  = ⟦ 1 ⟧< nonTrivial⇒n>1 _
+
+-- Projection from ℕ
+
+fromℕ : .{{ NonZero n }} → ℕ → ℕ< n
+fromℕ {n} m = ⟦ m % n ⟧< ℕ.m%n<n m n
+
+-- Destructors
+
+¬ℕ<[0] : ¬ ℕ< 0
+¬ℕ<[0] ()
+
+nonZeroIndex : ℕ< n → NonZero n
+nonZeroIndex {n = suc _} _ = _
+
+isBounded : (i : ℕ< n) → ⟦ i ⟧ < n
+isBounded (⟦ _ ⟧< i<n) = recompute (_ ℕ.<? _) i<n
+
+-- Mapping to ℕ
+
+toℕ : ℕ< n → ℕ
+toℕ = ⟦_⟧
+
+------------------------------------------------------------------------
+-- Conversion to and from `Fin n`
+
+toFin : ℕ< n → Fin n
+toFin (⟦ _ ⟧< i<n) = Fin.fromℕ< i<n
+
+fromFin : Fin n → ℕ< n
+fromFin i = ⟦ Fin.toℕ i ⟧< Fin.toℕ<n i
+
+------------------------------------------------------------------------
+-- Inverting `fromℕ`: a graph view
+
+data _/∼≡_ : ℕ → ℕ< n → Set where
+  ‵fromℕ : ∀ m (i : ℕ< n) → (⟦ i ⟧ + m * n) /∼≡ i
+
+------------------------------------------------------------------------
+-- Quotient equivalence relation on ℕ induced by `fromℕ`
+
+record _∼_ {n} (lhs rhs : ℕ) : Set where
+  constructor _,_
+  field
+    {k}    : ℕ< n
+    lhs/∼≡ : lhs /∼≡ k
+    rhs/∼≡ : rhs /∼≡ k
+
+≡-Modℕ : ℕ → Rel ℕ _
+≡-Modℕ n = _∼_ {n}
+
+syntax ≡-Modℕ n m o = m ≡ o modℕ n
+
+nonZeroModulus : (m ≡ o modℕ n) → NonZero n
+nonZeroModulus eq = nonZeroIndex k where open _∼_ eq
diff --git a/src/Data/Nat/Bounded/Properties.agda b/src/Data/Nat/Bounded/Properties.agda
new file mode 100644
index 0000000000..739b8bb8d4
--- /dev/null
+++ b/src/Data/Nat/Bounded/Properties.agda
@@ -0,0 +1,226 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of bounded natural numbers ℕ<
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Nat.Bounded.Properties where
+
+import Algebra.Definitions as Definitions
+open import Data.Fin.Base as Fin using (Fin)
+import Data.Fin.Properties as Fin
+open import Data.Nat.Base as ℕ
+import Data.Nat.DivMod as ℕ
+import Data.Nat.Properties as ℕ
+open import Data.Product.Base using (_,_)
+open import Function.Base using (id; _∘_; _$_; _on_)
+open import Function.Bundles using (_⤖_; mk⤖; _↔_; mk↔ₛ′)
+open import Function.Consequences.Propositional
+  using (inverseᵇ⇒bijective; strictlyInverseˡ⇒inverseˡ; strictlyInverseʳ⇒inverseʳ)
+open import Relation.Binary.Bundles using (PartialSetoid; Setoid)
+open import Relation.Binary.Structures using (IsPartialEquivalence; IsEquivalence)
+open import Relation.Binary.Core using (_⇒_)
+open import Relation.Binary.Definitions
+open import Relation.Binary.PropositionalEquality
+  hiding (isEquivalence; setoid)
+open import Relation.Nullary.Decidable.Core using (map′)
+
+open import Data.Nat.Bounded.Base as ℕ<
+
+private
+  variable
+    m n o : ℕ
+    i j k : ℕ< n
+
+
+------------------------------------------------------------------------
+-- Equality on values is propositional equality
+
+⟦0⟧≡0 : .{{_ : NonZero n}} → ⟦ ⟦0⟧< {n = n} ⟧ ≡ 0
+⟦0⟧≡0 {n = suc _} = refl
+
+⟦1⟧≡1 : .{{_ : NonTrivial n}} →
+        let instance _ = nonTrivial⇒nonZero n in ⟦ ⟦1⟧< {n = n} ⟧ ≡ 1
+⟦1⟧≡1 {n = 2+ _} = refl
+
+≡⇒⟦⟧≡⟦⟧ : _≡_ {A = ℕ< n} ⇒ (_≡_ on ⟦_⟧)
+≡⇒⟦⟧≡⟦⟧ = cong ⟦_⟧
+
+⟦⟧≡⟦⟧⇒≡ :  (_≡_ on ⟦_⟧) ⇒ _≡_ {A = ℕ< n}
+⟦⟧≡⟦⟧⇒≡ refl = refl
+
+fromℕ[n]≡0 : .{{_ : NonZero n}} → fromℕ n ≡ ⟦0⟧<
+fromℕ[n]≡0 {n} = ⟦⟧≡⟦⟧⇒≡ (ℕ.n%n≡0 n)
+
+module _ (m<n : m < n) where
+
+  private instance _ = ℕ.>-nonZero (ℕ.m<n⇒0<n m<n)
+
+  +-inverseˡ : fromℕ (n ∸ m + m) ≡ ⟦0⟧<
+  +-inverseˡ = trans (cong fromℕ (ℕ.m∸n+n≡m (ℕ.<⇒≤ m<n))) fromℕ[n]≡0
+
+  +-inverseʳ : fromℕ (m + (n ∸ m)) ≡ ⟦0⟧<
+  +-inverseʳ = trans (cong fromℕ (ℕ.m+[n∸m]≡n (ℕ.<⇒≤ m<n))) fromℕ[n]≡0
+
+  fromℕ≐⟦⟧< : fromℕ m ≡ ⟦ m ⟧< m<n
+  fromℕ≐⟦⟧< = ⟦⟧≡⟦⟧⇒≡ $ ℕ.m<n⇒m%n≡m m<n
+
+fromℕ∘toℕ≐id : (i : ℕ< n) → let instance _ = nonZeroIndex i
+               in fromℕ ⟦ i ⟧ ≡ i
+fromℕ∘toℕ≐id i = fromℕ≐⟦⟧< (ℕ<.isBounded i)
+
+infix 4 _≟_
+_≟_ : DecidableEquality (ℕ< n)
+i ≟ j = map′ ⟦⟧≡⟦⟧⇒≡ ≡⇒⟦⟧≡⟦⟧ (⟦ i ⟧ ℕ.≟ ⟦ j ⟧)
+
+------------------------------------------------------------------------
+-- Conversion to and from `Fin n`
+
+toFin∘fromFin≐id : toFin ∘ fromFin ≗ id {A = Fin n}
+toFin∘fromFin≐id i = Fin.fromℕ<-toℕ i (Fin.toℕ<n i)
+
+fromFin∘toFin≐id : fromFin ∘ toFin ≗ id {A = ℕ< n}
+fromFin∘toFin≐id (⟦ _ ⟧< i<n) = ⟦⟧≡⟦⟧⇒≡ (Fin.toℕ-fromℕ< i<n)
+
+boundedNat⤖Fin : ℕ< n ⤖ Fin n
+boundedNat⤖Fin = mk⤖ $ inverseᵇ⇒bijective $
+  strictlyInverseˡ⇒inverseˡ {f⁻¹ = fromFin} toFin toFin∘fromFin≐id
+  ,
+  strictlyInverseʳ⇒inverseʳ {f⁻¹ = fromFin} toFin fromFin∘toFin≐id
+
+boundedNat↔Fin : ℕ< n ↔ Fin n
+boundedNat↔Fin = mk↔ₛ′ toFin fromFin toFin∘fromFin≐id fromFin∘toFin≐id
+
+------------------------------------------------------------------------
+-- Inversion properties of the graph view of `fromℕ`
+
+module _ {m} {i : ℕ< n} where
+
+  private instance _ = nonZeroIndex i
+
+  _/∼≡fromℕ : fromℕ m ≡ i → m /∼≡ i
+  _/∼≡fromℕ = _/∼≡fromℕ′
+    where
+    _/∼≡fromℕ′ : .{{_ : NonZero n}} → fromℕ m ≡ i → m /∼≡ i
+    _/∼≡fromℕ′ refl = subst (_/∼≡ i) (sym (ℕ.m≡m%n+[m/n]*n m n)) (‵fromℕ (m / n) i)
+
+
+  _/∼≡fromℕ⁻¹ : m /∼≡ i → fromℕ m ≡ i
+  (‵fromℕ {n = n} m i) /∼≡fromℕ⁻¹ = ⟦⟧≡⟦⟧⇒≡ $
+    trans (ℕ.[m+kn]%n≡m%n ⟦ i ⟧ m n) (ℕ.m<n⇒m%n≡m (isBounded i))
+
+/∼≡-injective : m /∼≡ i → m /∼≡ j → i ≡ j
+/∼≡-injective m/∼≡i m/∼≡j = trans (sym (m/∼≡i /∼≡fromℕ⁻¹)) (m/∼≡j /∼≡fromℕ⁻¹)
+
+------------------------------------------------------------------------
+-- Properties of the quotient on ℕ induced by `fromℕ`
+
+n≡0-mod : .{{_ : NonZero n}} → n ≡ 0 modℕ n
+n≡0-mod = let r = fromℕ[n]≡0 /∼≡fromℕ in r , ‵fromℕ 0 ⟦0⟧<
+
+≡-mod-sym : Symmetric (≡-Modℕ n)
+≡-mod-sym (lhs , rhs) = rhs , lhs
+
+≡-mod-trans : Transitive (≡-Modℕ n)
+≡-mod-trans (lhs₁ , rhs₁) (lhs₂ , rhs₂)
+  with refl ← /∼≡-injective rhs₁ lhs₂ = lhs₁ , rhs₂
+
+isPartialEquivalence : IsPartialEquivalence (≡-Modℕ n)
+isPartialEquivalence = record { sym = ≡-mod-sym ; trans = ≡-mod-trans }
+
+partialSetoid : ℕ → PartialSetoid _ _
+partialSetoid n = record { _≈_ = ≡-Modℕ n ; isPartialEquivalence = isPartialEquivalence }
+
+≡-mod-refl : .{{NonZero n}} → Reflexive (≡-Modℕ n)
+≡-mod-refl {n} {m} = let r = erefl (fromℕ m) /∼≡fromℕ in r , r
+
+isEquivalence : .{{NonZero n}} → IsEquivalence (≡-Modℕ n)
+isEquivalence {n} = record
+  { refl = ≡-mod-refl
+  ; sym = ≡-mod-sym
+  ; trans = ≡-mod-trans
+  }
+
+setoid : .{{NonZero n}} → Setoid _ _
+setoid = record { isEquivalence = isEquivalence }
+
+≡-mod-reflexive : .{{NonZero n}} → _≡_ {A = ℕ} ⇒ (≡-Modℕ n)
+≡-mod-reflexive = reflexive where open IsEquivalence isEquivalence
+
+≡-mod⇒fromℕ≡fromℕ : (eq : m ≡ o modℕ n) →
+                    let instance _ = nonZeroModulus eq
+                    in fromℕ m ≡ fromℕ o
+≡-mod⇒fromℕ≡fromℕ (lhs/∼≡ , rhs/∼≡) = trans (lhs/∼≡ /∼≡fromℕ⁻¹) (sym (rhs/∼≡ /∼≡fromℕ⁻¹))
+
+≡-mod⇒%≡% : (eq : m ≡ o modℕ n) →
+            let instance _ = nonZeroModulus eq
+            in m % n ≡ o % n
+≡-mod⇒%≡% = ≡⇒⟦⟧≡⟦⟧ ∘ ≡-mod⇒fromℕ≡fromℕ
+
+fromℕ≡fromℕ⇒≡-mod : .{{_ : NonZero n}} → (_≡_ on fromℕ) ⇒ ≡-Modℕ n
+fromℕ≡fromℕ⇒≡-mod eq = eq /∼≡fromℕ , refl /∼≡fromℕ
+
+%≡%⇒≡-mod : .{{_ : NonZero n}} → (_≡_ on _% n) ⇒ ≡-Modℕ n
+%≡%⇒≡-mod eq = fromℕ≡fromℕ⇒≡-mod (⟦⟧≡⟦⟧⇒≡ eq)
+
+toℕ∘fromℕ≐id : .{{_ : NonZero n}} → (m : ℕ) → ⟦ fromℕ m ⟧ ≡ m modℕ n
+toℕ∘fromℕ≐id m = fromℕ≡fromℕ⇒≡-mod (fromℕ∘toℕ≐id (fromℕ m))
+
+------------------------------------------------------------------------
+-- Arithmetic properties of bounded numbers
+
+module _ (m<n : m < n) (o<n : o < n) where
+
+  private
+    instance
+      n≢ₘ0 = ℕ.>-nonZero (ℕ.m<n⇒0<n m<n)
+      n≢ₒ0 = ℕ.>-nonZero (ℕ.m<n⇒0<n o<n)
+
+  open ≡-Reasoning
+
+  ≡-mod⇒≡ : m ≡ o modℕ n → m ≡ o
+  ≡-mod⇒≡ eq = ≡⇒⟦⟧≡⟦⟧ $ begin
+    ⟦ m ⟧< m<n       ≡⟨ fromℕ≐⟦⟧< m<n ⟨
+    fromℕ {{n≢ₘ0}} m ≡⟨ ≡-mod⇒fromℕ≡fromℕ eq ⟩
+    fromℕ {{n≢ₒ0}} o ≡⟨ fromℕ≐⟦⟧< o<n ⟩
+    ⟦ o ⟧< o<n       ∎
+
+module _ .{{_ : NonZero n}} (m o : ℕ) where
+
+  open ≡-Reasoning
+
+  +-distrib-% : ((m % n) + (o % n)) ≡ (m + o) modℕ n
+  +-distrib-% = %≡%⇒≡-mod $ begin
+    (m % n + o % n) % n     ≡⟨ ℕ.%-distribˡ-+ m o n ⟨
+    (m + o) % n             ∎
+
+  +-distribˡ-% : ((m % n) + o) ≡ (m + o) modℕ n
+  +-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ (begin
+    (m % n + o) % n         ≡⟨ ℕ.%-distribˡ-+ (m % n) o n ⟩
+    (m % n % n + o % n) % n ≡⟨ cong ((_% n) ∘ (_+ o % n)) (ℕ.m%n%n≡m%n m n) ⟩
+    (m % n + o % n) % n     ∎)) +-distrib-%
+
+  +-distribʳ-% : (m + (o % n)) ≡ (m + o) modℕ n
+  +-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin
+    (m + o % n) % n         ≡⟨ ℕ.%-distribˡ-+ m (o % n) n ⟩
+    (m % n + o % n % n) % n ≡⟨ cong ((_% n) ∘ (m % n +_)) (ℕ.m%n%n≡m%n o n) ⟩
+    (m % n + o % n) % n     ∎) +-distrib-%
+
+  *-distrib-% : ((m % n) * (o % n)) ≡ (m * o) modℕ n
+  *-distrib-% = %≡%⇒≡-mod $ begin
+    ((m % n) * (o % n)) % n ≡⟨ ℕ.%-distribˡ-* m o n ⟨
+    (m * o) % n             ∎
+
+  *-distribˡ-% : ((m % n) * o) ≡ (m * o) modℕ n
+  *-distribˡ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin
+    (m % n * o) % n           ≡⟨ ℕ.%-distribˡ-* (m % n) o n ⟩
+    (m % n % n * (o % n)) % n ≡⟨ cong ((_% n) ∘ (_* (o % n))) (ℕ.m%n%n≡m%n m n) ⟩
+    (m % n * (o % n)) % n     ∎) *-distrib-%
+
+  *-distribʳ-% : (m * (o % n)) ≡ (m * o) modℕ n
+  *-distribʳ-% = ≡-mod-trans (%≡%⇒≡-mod $ begin
+    (m * (o % n)) % n         ≡⟨ ℕ.%-distribˡ-* m (o % n) n ⟩
+    (m % n * (o % n % n)) % n ≡⟨ cong ((_% n) ∘ (m % n *_)) (ℕ.m%n%n≡m%n o n) ⟩
+    (m % n * (o % n)) % n     ∎) *-distrib-%