diff --git a/CHANGELOG.md b/CHANGELOG.md
index 479eb395bc..af7a35ea0f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -645,10 +645,14 @@ Non-backwards compatible changes
 * To make it easier to use, reason about and read, the definition has been
   changed to:
   ```agda
-  Prime 0 = ⊥
-  Prime 1 = ⊥
-  Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
+  record Prime (p : ℕ) : Set where
+    constructor prime
+    field
+      .{{nontrivial}} : NonTrivial p
+      notComposite    : ¬ Composite p
   ```
+  where `Composite` is now defined as the diagonal of the new relation
+  `_HasNonTrivialDivisorLessThan_` in `Data.Nat.Divisibility.Core`.
 
 ### Changes to operation reduction behaviour in `Data.Rational(.Unnormalised)`
 
@@ -2731,6 +2735,18 @@ Additions to existing modules
   s≤″s⁻¹ : suc m ≤″ suc n → m ≤″ n
   s<″s⁻¹ : suc m <″ suc n → m <″ n
 
+  pattern 2+ n = suc (suc n)
+  pattern 1<2+n {n} = s<s (z<s {n})
+
+  NonTrivial            : Pred ℕ 0ℓ
+  instance nonTrivial   : NonTrivial (2+ n)
+  n>1⇒nonTrivial        : 1 < n → NonTrivial n
+  nonZero⇒≢1⇒nonTrivial : .{{NonZero n}} → n ≢ 1 → NonTrivial n
+  recompute-nonTrivial  : .{{NonTrivial n}} → NonTrivial n
+  nonTrivial⇒nonZero    : .{{NonTrivial n}} → NonZero n
+  nonTrivial⇒n>1        : .{{NonTrivial n}} → 1 < n
+  nonTrivial⇒≢1         : .{{NonTrivial n}} → n ≢ 1
+
   _⊔′_ : ℕ → ℕ → ℕ
   _⊓′_ : ℕ → ℕ → ℕ
   ∣_-_∣′ : ℕ → ℕ → ℕ
@@ -2756,20 +2772,42 @@ Additions to existing modules
   <-asym : Asymmetric _<_
   ```
 
-* Added a new pattern synonym to `Data.Nat.Divisibility.Core`:
+* Added a new pattern synonym and a new definition to `Data.Nat.Divisibility.Core`:
   ```agda
   pattern divides-refl q = divides q refl
+  record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where
+  ```
+
+* Added new proofs to `Data.Nat.Divisibility`:
+  ```agda
+  hasNonTrivialDivisor-≢ : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n
+  hasNonTrivialDivisor-∣ : m HasNonTrivialDivisorLessThan n → m ∣ o → o HasNonTrivialDivisorLessThan n
+  hasNonTrivialDivisor-≤ : m HasNonTrivialDivisorLessThan n → n ≤ o → m HasNonTrivialDivisorLessThan o
   ```
 
-* Added new definitions and proofs to `Data.Nat.Primality`:
+* Added new definitions, smart constructors and proofs to `Data.Nat.Primality`:
   ```agda
-  Composite        : ℕ → Set
-  composite?       : Decidable Composite
-  composite⇒¬prime : Composite n → ¬ Prime n
-  ¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n
-  prime⇒¬composite : Prime n → ¬ Composite n
-  ¬prime⇒composite : 2 ≤ n → ¬ Prime n → Composite n
-  euclidsLemma     : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
+  infix 10 _Rough_
+  _Rough_           : ℕ → Pred ℕ _
+  0-rough           : 0 Rough n
+  1-rough           : 1 Rough n
+  2-rough           : 2 Rough n
+  rough⇒≤           : .{{NonTrivial n}} → m Rough n → m ≤ n
+  ∤⇒rough-suc        : m ∤ n → m Rough n → (suc m) Rough n
+  rough∧∣⇒rough     : m Rough o → n ∣ o → m Rough n
+  Composite         : ℕ → Set
+  composite-≢       : .{{NonTrivial d}} → .{{NonZero n}} → d ≢ n → d ∣ n → Composite n
+  composite-∣       : .{{NonZero n}} → Composite m → m ∣ n → Composite n
+  composite?        : Decidable Composite
+  Irreducible       : ℕ → Set
+  irreducible?      : Decidable Irreducible
+  composite⇒¬prime  : Composite n → ¬ Prime n
+  ¬composite⇒prime  : .{{NonTrivial n} → ¬ Composite n → Prime n
+  prime⇒¬composite  : Prime n → ¬ Composite n
+  ¬prime⇒composite  : .{{NonTrivial n} → ¬ Prime n → Composite n
+  prime⇒irreducible : Prime p → Irreducible p
+  irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p
+  euclidsLemma      : Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
   ```
 
 * Added new proofs in `Data.Nat.Properties`:
@@ -2779,8 +2817,12 @@ Additions to existing modules
   n+1+m≢m   : n + suc m ≢ m
   m*n≡0⇒m≡0 : .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
   n>0⇒n≢0   : n > 0 → n ≢ 0
-  m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
   m*n≢0     : .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
+  m*n≢0⇒m≢0 : .{{NonZero (m * n)}} → NonZero m
+  m*n≢0⇒n≢0 : .{{NonZero (m * n)}} → NonZero n
+  m≢0∧n>1⇒m*n>1 : .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n)
+  n≢0∧m>1⇒m*n>1 : .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n)
+  m^n≢0     : .{{_ : NonZero m}} → NonZero (m ^ n)
   m≤n⇒n∸m≤n : m ≤ n → n ∸ m ≤ n
 
   s<s-injective : s<s p ≡ s<s q → p ≡ q
@@ -2788,7 +2830,7 @@ Additions to existing modules
   m<1+n⇒m<n∨m≡n : m < suc n → m < n ⊎ m ≡ n
 
   pred-mono-≤   : m ≤ n → pred m ≤ pred n
-  pred-mono-<   : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+  pred-mono-<   : .{{_ : NonZero m}} → m < n → pred m < pred n
 
   z<′s : zero <′ suc n
   s<′s : m <′ n → suc m <′ suc n
@@ -2829,7 +2871,7 @@ Additions to existing modules
   ⊓≡⊓′ : m ⊓ n ≡ m ⊓′ n
   ∣-∣≡∣-∣′ : ∣ m - n ∣ ≡ ∣ m - n ∣′
 
-  nonZero? : Decidable NonZero
+  nonTrivial? : Decidable NonTrivial
   eq? : A ↣ ℕ → DecidableEquality A
   ≤-<-connex : Connex _≤_ _<_
   ≥->-connex : Connex _≥_ _>_
@@ -2855,21 +2897,21 @@ Additions to existing modules
   m%n≤n           : .{{_ : NonZero n}} → m % n ≤ n
   m*n/m!≡n/[m∸1]! : .{{_ : NonZero m}} → m * n / m ! ≡ n / (pred m) !
 
-  %-congˡ             : .⦃ _ : NonZero o ⦄ → m ≡ n → m % o ≡ n % o
-  %-congʳ             : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ≡ n → o % m ≡ o % n
-  m≤n⇒[n∸m]%m≡n%m     : .⦃ _ : NonZero m ⦄ → m ≤ n → (n ∸ m) % m ≡ n % m
-  m*n≤o⇒[o∸m*n]%n≡o%n : .⦃ _ : NonZero n ⦄ → m * n ≤ o → (o ∸ m * n) % n ≡ o % n
-  m∣n⇒o%n%m≡o%m       : .⦃ _ : NonZero m ⦄ .⦃ _ : NonZero n ⦄ → m ∣ n → o % n % m ≡ o % m
-  m<n⇒m%n≡m           : .⦃ _ : NonZero n ⦄ → m < n → m % n ≡ m
-  m*n/o*n≡m/o         : .⦃ _ : NonZero o ⦄ ⦃ _ : NonZero (o * n) ⦄ → m * n / (o * n) ≡ m / o
-  m<n*o⇒m/o<n         : .⦃ _ : NonZero o ⦄ → m < n * o → m / o < n
-  [m∸n]/n≡m/n∸1       : .⦃ _ : NonZero n ⦄ → (m ∸ n) / n ≡ pred (m / n)
-  [m∸n*o]/o≡m/o∸n     : .⦃ _ : NonZero o ⦄ → (m ∸ n * o) / o ≡ m / o ∸ n
-  m/n/o≡m/[n*o]       : .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄ .⦃ _ : NonZero (n * o) ⦄ → m / n / o ≡ m / (n * o)
-  m%[n*o]/o≡m/o%n     : .⦃ _ : NonZero n ⦄ .⦃ _ : NonZero o ⦄ ⦃ _ : NonZero (n * o) ⦄ → m % (n * o) / o ≡ m / o % n
-  m%n*o≡m*o%[n*o]     : .⦃ _ : NonZero n ⦄ ⦃ _ : NonZero (n * o) ⦄ → m % n * o ≡ m * o % (n * o)
+  %-congˡ             : .{{_ : NonZero o}} → m ≡ n → m % o ≡ n % o
+  %-congʳ             : .{{_ : NonZero m}} .{{_ : NonZero n}} → m ≡ n → o % m ≡ o % n
+  m≤n⇒[n∸m]%m≡n%m     : .{{_ : NonZero m}} → m ≤ n → (n ∸ m) % m ≡ n % m
+  m*n≤o⇒[o∸m*n]%n≡o%n : .{{_ : NonZero n}} → m * n ≤ o → (o ∸ m * n) % n ≡ o % n
+  m∣n⇒o%n%m≡o%m       : .{{_ : NonZero m}} .{{_ : NonZero n}} → m ∣ n → o % n % m ≡ o % m
+  m<n⇒m%n≡m           : .{{_ : NonZero n}} → m < n → m % n ≡ m
+  m*n/o*n≡m/o         : .{{_ : NonZero o}} {{_ : NonZero (o * n)}} → m * n / (o * n) ≡ m / o
+  m<n*o⇒m/o<n         : .{{_ : NonZero o}} → m < n * o → m / o < n
+  [m∸n]/n≡m/n∸1       : .{{_ : NonZero n}} → (m ∸ n) / n ≡ pred (m / n)
+  [m∸n*o]/o≡m/o∸n     : .{{_ : NonZero o}} → (m ∸ n * o) / o ≡ m / o ∸ n
+  m/n/o≡m/[n*o]       : .{{_ : NonZero n}} .{{_ : NonZero o}} .{{_ : NonZero (n * o)}} → m / n / o ≡ m / (n * o)
+  m%[n*o]/o≡m/o%n     : .{{_ : NonZero n}} .{{_ : NonZero o}} {{_ : NonZero (n * o)}} → m % (n * o) / o ≡ m / o % n
+  m%n*o≡m*o%[n*o]     : .{{_ : NonZero n}} {{_ : NonZero (n * o)}} → m % n * o ≡ m * o % (n * o)
 
-  [m*n+o]%[p*n]≡[m*n]%[p*n]+o : ⦃ _ : NonZero (p * n) ⦄ → o < n → (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o
+  [m*n+o]%[p*n]≡[m*n]%[p*n]+o : {{_ : NonZero (p * n)}} → o < n → (m * n + o) % (p * n) ≡ (m * n) % (p * n) + o
   ```
 
 * Added new proofs in `Data.Nat.Divisibility`:
@@ -3606,7 +3648,9 @@ This is a full list of proofs that have changed form to use irrelevant instance
 
 * In `Data.Nat.Coprimality`:
   ```
-  Bézout-coprime : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j
+  ¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n)
+  Bézout-coprime  : ∀ {i j d} → Bézout.Identity (suc d) (i * suc d) (j * suc d) → Coprime i j
+  prime⇒coprime   : ∀ m → Prime m → ∀ n → 0 < n → n < m → Coprime m n
   ```
 
 * In `Data.Nat.Divisibility`
diff --git a/src/Data/Nat/Base.agda b/src/Data/Nat/Base.agda
index f2755c55fc..6135cfe01d 100644
--- a/src/Data/Nat/Base.agda
+++ b/src/Data/Nat/Base.agda
@@ -21,6 +21,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core
   using (_≡_; _≢_; refl)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
+open import Relation.Unary using (Pred)
 
 ------------------------------------------------------------------------
 -- Types
@@ -28,6 +29,9 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 open import Agda.Builtin.Nat public
   using (zero; suc) renaming (Nat to ℕ)
 
+--smart constructor
+pattern 2+ n = suc (suc n)
+
 ------------------------------------------------------------------------
 -- Boolean equality relation
 
@@ -59,8 +63,9 @@ m < n = suc m ≤ n
 
 -- Smart constructors of _<_
 
-pattern z<s {n}         = s≤s (z≤n {n})
+pattern z<s     {n}     = s≤s (z≤n {n})
 pattern s<s {m} {n} m<n = s≤s {m} {n} m<n
+pattern sz<ss   {n}     = s<s (z<s {n})
 
 -- Smart destructors of _≤_, _<_
 
@@ -72,7 +77,7 @@ s<s⁻¹ (s<s m<n) = m<n
 
 
 ------------------------------------------------------------------------
--- other ordering relations
+-- Other derived ordering relations
 
 _≥_ : Rel ℕ 0ℓ
 m ≥ n = n ≤ m
@@ -95,13 +100,19 @@ a ≯ b = ¬ a > b
 ------------------------------------------------------------------------
 -- Simple predicates
 
--- Defining `NonZero` in terms of `T` and therefore ultimately `⊤` and
--- `⊥` allows Agda to automatically infer nonZero-ness for any natural
--- of the form `suc n`. Consequently in many circumstances this
--- eliminates the need to explicitly pass a proof when the NonZero
--- argument is either an implicit or an instance argument.
+-- Defining these predicates in terms of `T` and therefore ultimately
+-- `⊤` and `⊥` allows Agda to automatically infer them for any natural
+-- of the correct form. Consequently in many circumstances this
+-- eliminates the need to explicitly pass a proof when the predicate
+-- argument is either an implicit or an instance argument. See `_/_`
+-- and `_%_` further down this file for examples.
 --
--- See `Data.Nat.DivMod` for an example.
+-- Furthermore, defining these predicates as single-field records
+-- (rather defining them directly as the type of their field) is
+-- necessary as the current version of Agda is far better at
+-- reconstructing meta-variable values for the record parameters.
+
+-- A predicate saying that a number is not equal to 0.
 
 record NonZero (n : ℕ) : Set where
   field
@@ -130,6 +141,34 @@ instance
 >-nonZero⁻¹ : ∀ n → .{{NonZero n}} → n > 0
 >-nonZero⁻¹ (suc n) = z<s
 
+-- The property of being a non-zero, non-unit
+
+record NonTrivial (n : ℕ) : Set where
+  field
+    nonTrivial : T (1 <ᵇ n)
+
+-- Instances
+
+instance
+  nonTrivial : ∀ {n} → NonTrivial (2+ n)
+  nonTrivial = _
+
+-- Constructors
+
+n>1⇒nonTrivial : ∀ {n} → n > 1 → NonTrivial n
+n>1⇒nonTrivial sz<ss = _
+
+-- Destructors
+
+nonTrivial⇒nonZero : ∀ n → .{{NonTrivial n}} → NonZero n
+nonTrivial⇒nonZero (2+ _) = _
+
+nonTrivial⇒n>1 : ∀ n → .{{NonTrivial n}} → n > 1
+nonTrivial⇒n>1 (2+ _) = sz<ss
+
+nonTrivial⇒≢1 : ∀ {n} → .{{NonTrivial n}} → n ≢ 1
+nonTrivial⇒≢1 {{()}} refl
+
 ------------------------------------------------------------------------
 -- Raw bundles
 
diff --git a/src/Data/Nat/Coprimality.agda b/src/Data/Nat/Coprimality.agda
index 1df320ea96..f385944f50 100644
--- a/src/Data/Nat/Coprimality.agda
+++ b/src/Data/Nat/Coprimality.agda
@@ -8,7 +8,6 @@
 
 module Data.Nat.Coprimality where
 
-open import Data.Empty
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD
@@ -17,15 +16,18 @@ open import Data.Nat.Primality
 open import Data.Nat.Properties
 open import Data.Nat.DivMod
 open import Data.Product.Base as Prod
+open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Function.Base using (_∘_)
 open import Level using (0ℓ)
 open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; _≢_; refl; trans; cong; subst)
-open import Relation.Nullary as Nullary hiding (recompute)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary as Nullary using (¬_; contradiction; yes ; no)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Symmetric; Decidable)
 
+private
+  variable d m n o p : ℕ
+
 open ≤-Reasoning
 
 ------------------------------------------------------------------------
@@ -35,22 +37,22 @@ open ≤-Reasoning
 -- prime), i.e. if their only common divisor is 1.
 
 Coprime : Rel ℕ 0ℓ
-Coprime m n = ∀ {i} → i ∣ m × i ∣ n → i ≡ 1
+Coprime m n = ∀ {d} → d ∣ m × d ∣ n → d ≡ 1
 
 ------------------------------------------------------------------------
 -- Relationship between GCD and coprimality
 
-coprime⇒GCD≡1 : ∀ {m n} → Coprime m n → GCD m n 1
-coprime⇒GCD≡1 {m} {n} c = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ c)
+coprime⇒GCD≡1 : Coprime m n → GCD m n 1
+coprime⇒GCD≡1 {m} {n} coprime = GCD.is (1∣ m , 1∣ n) (∣-reflexive ∘ coprime)
 
-GCD≡1⇒coprime : ∀ {m n} → GCD m n 1 → Coprime m n
+GCD≡1⇒coprime : GCD m n 1 → Coprime m n
 GCD≡1⇒coprime g cd with divides q eq ← GCD.greatest g cd
   = m*n≡1⇒n≡1 q _ (P.sym eq)
 
-coprime⇒gcd≡1 : ∀ {m n} → Coprime m n → gcd m n ≡ 1
+coprime⇒gcd≡1 : Coprime m n → gcd m n ≡ 1
 coprime⇒gcd≡1 coprime = GCD.unique (gcd-GCD _ _) (coprime⇒GCD≡1 coprime)
 
-gcd≡1⇒coprime : ∀ {m n} → gcd m n ≡ 1 → Coprime m n
+gcd≡1⇒coprime : gcd m n ≡ 1 → Coprime m n
 gcd≡1⇒coprime gcd≡1 = GCD≡1⇒coprime (subst (GCD _ _) gcd≡1 (gcd-GCD _ _))
 
 coprime-/gcd : ∀ m n .{{_ : NonZero (gcd m n)}} →
@@ -67,14 +69,14 @@ private
   0≢1 : 0 ≢ 1
   0≢1 ()
 
-  2+≢1 : ∀ {n} → suc (suc n) ≢ 1
+  2+≢1 : ∀ {n} → 2+ n ≢ 1
   2+≢1 ()
 
 coprime? : Decidable Coprime
-coprime? i j with mkGCD i j
-... | (0           , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime⇒GCD≡1)
-... | (1           , g) = yes (GCD≡1⇒coprime g)
-... | (suc (suc d) , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)
+coprime? m n with mkGCD m n
+... | (0    , g) = no  (0≢1  ∘ GCD.unique g ∘ coprime⇒GCD≡1)
+... | (1    , g) = yes (GCD≡1⇒coprime g)
+... | (2+ _ , g) = no  (2+≢1 ∘ GCD.unique g ∘ coprime⇒GCD≡1)
 
 ------------------------------------------------------------------------
 -- Other basic properties
@@ -86,21 +88,21 @@ coprime? i j with mkGCD i j
 
 -- Nothing except for 1 is coprime to 0.
 
-0-coprimeTo-m⇒m≡1 : ∀ {m} → Coprime 0 m → m ≡ 1
-0-coprimeTo-m⇒m≡1 {m} c = c (m ∣0 , ∣-refl)
+0-coprimeTo-m⇒m≡1 : Coprime 0 m → m ≡ 1
+0-coprimeTo-m⇒m≡1 {m} coprime = coprime (m ∣0 , ∣-refl)
 
-¬0-coprimeTo-2+ : ∀ {n} → ¬ Coprime 0 (2 + n)
-¬0-coprimeTo-2+ coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) λ()
+¬0-coprimeTo-2+ : .{{NonTrivial n}} → ¬ Coprime 0 n
+¬0-coprimeTo-2+ {n} coprime = contradiction (0-coprimeTo-m⇒m≡1 coprime) (nonTrivial⇒≢1 {n})
 
 -- If m and n are coprime, then n + m and n are also coprime.
 
-coprime-+ : ∀ {m n} → Coprime m n → Coprime (n + m) n
-coprime-+ c (d₁ , d₂) = c (∣m+n∣m⇒∣n d₁ d₂ , d₂)
+coprime-+ : Coprime m n → Coprime (n + m) n
+coprime-+ coprime (d₁ , d₂) = coprime (∣m+n∣m⇒∣n d₁ d₂ , d₂)
 
 -- Recomputable
 
-recompute : ∀ {n d} → .(Coprime n d) → Coprime n d
-recompute {n} {d} c = Nullary.recompute (coprime? n d) c
+recompute : .(Coprime n d) → Coprime n d
+recompute {n} {d} coprime = Nullary.recompute (coprime? n d) coprime
 
 ------------------------------------------------------------------------
 -- Relationship with Bezout's lemma
@@ -108,8 +110,8 @@ recompute {n} {d} c = Nullary.recompute (coprime? n d) c
 -- If the "gcd" in Bézout's identity is non-zero, then the "other"
 -- divisors are coprime.
 
-Bézout-coprime : ∀ {i j d} .{{_ : NonZero d}} →
-                 Bézout.Identity d (i * d) (j * d) → Coprime i j
+Bézout-coprime : .{{NonZero d}} →
+                 Bézout.Identity d (m * d) (n * d) → Coprime m n
 Bézout-coprime {d = suc _} (Bézout.+- x y eq) (divides-refl q₁ , divides-refl q₂) =
   lem₁₀ y q₂ x q₁ eq
 Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-refl q₂) =
@@ -117,21 +119,20 @@ Bézout-coprime {d = suc _} (Bézout.-+ x y eq) (divides-refl q₁ , divides-ref
 
 -- Coprime numbers satisfy Bézout's identity.
 
-coprime-Bézout : ∀ {i j} → Coprime i j → Bézout.Identity 1 i j
+coprime-Bézout : Coprime m n → Bézout.Identity 1 m n
 coprime-Bézout = Bézout.identity ∘ coprime⇒GCD≡1
 
--- If i divides jk and is coprime to j, then it divides k.
+-- If m divides n*o and is coprime to n, then it divides o.
 
-coprime-divisor : ∀ {k i j} → Coprime i j → i ∣ j * k → i ∣ k
-coprime-divisor {k} c (divides q eq′) with coprime-Bézout c
-... | Bézout.+- x y eq = divides (x * k ∸ y * q) (lem₈ x y eq eq′)
-... | Bézout.-+ x y eq = divides (y * q ∸ x * k) (lem₉ x y eq eq′)
+coprime-divisor : Coprime m n → m ∣ n * o → m ∣ o
+coprime-divisor {o = o} c (divides q eq′) with coprime-Bézout c
+... | Bézout.+- x y eq = divides (x * o ∸ y * q) (lem₈ x y eq eq′)
+... | Bézout.-+ x y eq = divides (y * q ∸ x * o) (lem₉ x y eq eq′)
 
--- If d is a common divisor of mk and nk, and m and n are coprime,
--- then d divides k.
+-- If d is a common divisor of m*o and n*o, and m and n are coprime,
+-- then d divides o.
 
-coprime-factors : ∀ {d m n k} →
-                  Coprime m n → d ∣ m * k × d ∣ n * k → d ∣ k
+coprime-factors : Coprime m n → d ∣ m * o × d ∣ n * o → d ∣ o
 coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout c
 ... | Bézout.+- x y eq = divides (x * q₁ ∸ y * q₂) (lem₁₁ x y eq eq₁ eq₂)
 ... | Bézout.-+ x y eq = divides (y * q₂ ∸ x * q₁) (lem₁₁ y x eq eq₂ eq₁)
@@ -139,11 +140,7 @@ coprime-factors c (divides q₁ eq₁ , divides q₂ eq₂) with coprime-Bézout
 ------------------------------------------------------------------------
 -- Primality implies coprimality.
 
-prime⇒coprime : ∀ m → Prime m →
-                ∀ n → 0 < n → n < m → Coprime m n
-prime⇒coprime (suc (suc _)) p _ _ _ {0} (0∣m , _) =
-  contradiction (0∣⇒≡0 0∣m) λ()
-prime⇒coprime (suc (suc _)) _ _ _ _ {1} _         = refl
-prime⇒coprime (suc (suc _)) p (suc _) _ n<m {(suc (suc _))} (d∣m , d∣n) =
-  contradiction d∣m (p 2≤d d<m)
-  where 2≤d = s≤s (s≤s z≤n); d<m = <-≤-trans (s≤s (∣⇒≤ d∣n)) n<m
+prime⇒coprime : Prime p → .{{NonZero n}} → n < p → Coprime p n
+prime⇒coprime p n<p (d∣p , d∣n) with prime⇒irreducible p d∣p
+... | inj₁ d≡1      = d≡1
+... | inj₂ d≡p@refl = contradiction n<p (≤⇒≯ (∣⇒≤ d∣n))
diff --git a/src/Data/Nat/Divisibility.agda b/src/Data/Nat/Divisibility.agda
index bb30716e01..9083642f80 100644
--- a/src/Data/Nat/Divisibility.agda
+++ b/src/Data/Nat/Divisibility.agda
@@ -12,11 +12,10 @@ open import Algebra
 open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Properties
-open import Data.Unit.Base using (tt)
 open import Function.Base using (_∘′_; _$_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (0ℓ)
-open import Relation.Nullary.Decidable as Dec using (False; yes; no)
+open import Relation.Nullary.Decidable as Dec using (yes; no)
 open import Relation.Nullary.Negation.Core using (contradiction)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.Bundles using (Preorder; Poset)
@@ -308,3 +307,27 @@ m≤n⇒m!∣n! m≤n = help (≤⇒≤′ m≤n)
   help : ∀ {m n} → m ≤′ n → m ! ∣ n !
   help {m} {n}     ≤′-refl        = ∣-refl
   help {m} {suc n} (≤′-step m≤′n) = ∣n⇒∣m*n (suc n) (help m≤′n)
+
+------------------------------------------------------------------------
+-- Properties of _BoundedNonTrivialDivisor_
+
+-- Smart constructor
+
+hasNonTrivialDivisor-≢ : ∀ {d n} → .{{NonTrivial d}} → .{{NonZero n}} →
+                         d ≢ n → d ∣ n → n HasNonTrivialDivisorLessThan n
+hasNonTrivialDivisor-≢ d≢n d∣n
+  = hasNonTrivialDivisor (≤∧≢⇒< (∣⇒≤ d∣n) d≢n) d∣n
+
+-- Monotonicity wrt ∣
+
+hasNonTrivialDivisor-∣ : ∀ {m n o} → m HasNonTrivialDivisorLessThan n → m ∣ o →
+                         o HasNonTrivialDivisorLessThan n
+hasNonTrivialDivisor-∣ (hasNonTrivialDivisor d<n d∣m) n∣o
+  = hasNonTrivialDivisor d<n (∣-trans d∣m n∣o)
+
+-- Monotonicity wrt ≤
+
+hasNonTrivialDivisor-≤ : ∀ {m n o} → m HasNonTrivialDivisorLessThan n → n ≤ o →
+                             m HasNonTrivialDivisorLessThan o
+hasNonTrivialDivisor-≤ (hasNonTrivialDivisor d<n d∣m) m≤o =
+  hasNonTrivialDivisor (<-≤-trans d<n m≤o) d∣m
diff --git a/src/Data/Nat/Divisibility/Core.agda b/src/Data/Nat/Divisibility/Core.agda
index 2f8cdbe241..58ef913a5f 100644
--- a/src/Data/Nat/Divisibility/Core.agda
+++ b/src/Data/Nat/Divisibility/Core.agda
@@ -12,7 +12,7 @@
 
 module Data.Nat.Divisibility.Core where
 
-open import Data.Nat.Base using (ℕ; _*_)
+open import Data.Nat.Base using (ℕ; _*_; _<_; NonTrivial)
 open import Data.Nat.Properties
 open import Level using (0ℓ)
 open import Relation.Nullary.Negation using (¬_)
@@ -21,7 +21,7 @@ open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; sym; cong₂; module ≡-Reasoning)
 
 ------------------------------------------------------------------------
--- Definition
+-- Main definition
 --
 -- m ∣ n is inhabited iff m divides n. Some sources, like Hardy and
 -- Wright's "An Introduction to the Theory of Numbers", require m to
@@ -40,10 +40,25 @@ open _∣_ using (quotient) public
 _∤_ : Rel ℕ 0ℓ
 m ∤ n = ¬ (m ∣ n)
 
--- smart constructor
+-- Smart constructor
 
 pattern divides-refl q = divides q refl
 
+------------------------------------------------------------------------
+-- Restricted divisor relation
+
+-- Relation for having a non-trivial divisor below a given bound.
+-- Useful when reasoning about primality.
+infix 10 _HasNonTrivialDivisorLessThan_
+
+record _HasNonTrivialDivisorLessThan_ (m n : ℕ) : Set where
+  constructor hasNonTrivialDivisor
+  field
+    {divisor}       : ℕ
+    .{{nontrivial}} : NonTrivial divisor
+    divisor-<       : divisor < n
+    divisor-∣       : divisor ∣ m
+
 ------------------------------------------------------------------------
 -- Basic properties
 
diff --git a/src/Data/Nat/Primality.agda b/src/Data/Nat/Primality.agda
index 361df42b73..620f0c87b0 100644
--- a/src/Data/Nat/Primality.agda
+++ b/src/Data/Nat/Primality.agda
@@ -8,92 +8,245 @@
 
 module Data.Nat.Primality where
 
-open import Data.Empty using (⊥)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
 open import Data.Nat.Properties
-open import Data.Product.Base using (∃; _×_; map₂; _,_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)
+open import Function.Bundles using (_⇔_; mk⇔)
 open import Relation.Nullary.Decidable as Dec
-  using (yes; no; from-yes; ¬?; decidable-stable; _×-dec_; _→-dec_)
-open import Relation.Nullary.Negation using (¬_; contradiction)
-open import Relation.Unary using (Decidable)
+  using (yes; no; from-yes; from-no; ¬?; _×-dec_; _⊎-dec_; _→-dec_; decidable-stable)
+open import Relation.Nullary.Negation using (¬_; contradiction; contradiction₂)
+open import Relation.Unary using (Pred; Decidable)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality
-  using (refl; cong)
+  using (_≡_; _≢_; refl; cong)
 
 private
   variable
-    n : ℕ
+    d m n o p : ℕ
+
+  recompute-nonTrivial : .{{NonTrivial n}} → NonTrivial n
+  recompute-nonTrivial {n} {{nontrivial}} =
+    Dec.recompute (nonTrivial? n) nontrivial
 
 ------------------------------------------------------------------------
 -- Definitions
+------------------------------------------------------------------------
+
+-- The positive/existential relation `BoundedNonTrivialDivisor` is
+-- the basis for the whole development, as it captures the possible
+-- non-trivial divisors of a given number; its complement, `Rough`,
+-- therefore sets *lower* bounds on any possible such divisors.
 
--- Definition of compositeness
+-- The predicate `Composite` is then defined as the 'diagonal' instance
+-- of `BoundedNonTrivialDivisor`, while `Prime` is essentially defined as
+-- the complement of `Composite`. Finally, `Irreducible` is the positive
+-- analogue of `Prime`.
 
-Composite : ℕ → Set
-Composite 0 = ⊥
-Composite 1 = ⊥
-Composite n = ∃ λ d → 2 ≤ d × d < n × d ∣ n
+------------------------------------------------------------------------
+-- Roughness
 
--- Definition of primality.
+-- A number is m-rough if all its non-trivial divisors are bounded below
+-- by m.
+infix 10 _Rough_
 
-Prime : ℕ → Set
-Prime 0 = ⊥
-Prime 1 = ⊥
-Prime n = ∀ {d} → 2 ≤ d → d < n → d ∤ n
+_Rough_ : ℕ → Pred ℕ _
+m Rough n = ¬ (n HasNonTrivialDivisorLessThan m)
 
 ------------------------------------------------------------------------
--- Decidability
+-- Compositeness
 
-composite? : Decidable Composite
-composite? 0               = no λ()
-composite? 1               = no λ()
-composite? n@(suc (suc _)) = Dec.map′
-  (map₂ λ { (a , b , c) → (b , a , c)})
-  (map₂ λ { (a , b , c) → (b , a , c)})
-  (anyUpTo? (λ d → 2 ≤? d ×-dec d ∣? n) n)
+-- A number is composite if it has a proper non-trivial divisor.
+Composite : Pred ℕ _
+Composite n = n HasNonTrivialDivisorLessThan n
 
-prime? : Decidable Prime
-prime? 0               = no λ()
-prime? 1               = no λ()
-prime? n@(suc (suc _)) = Dec.map′
-  (λ f {d} → flip (f {d}))
-  (λ f {d} → flip (f {d}))
-  (allUpTo? (λ d → 2 ≤? d →-dec ¬? (d ∣? n)) n)
+-- A shorter pattern synonym for the record constructor producing a
+-- witness for `Composite`.
+pattern
+  composite {d} d<n d∣n = hasNonTrivialDivisor {divisor = d} d<n d∣n
 
 ------------------------------------------------------------------------
--- Relationships between compositeness and primality
+-- Primality
 
-composite⇒¬prime : Composite n → ¬ Prime n
-composite⇒¬prime {n@(suc (suc _))} (d , 2≤d , d<n , d∣n) n-prime =
-  n-prime 2≤d d<n d∣n
+-- Prime as the complement of Composite (and hence the diagonal of Rough
+-- as defined above). The constructor `prime` takes a proof `notComposite`
+-- that NonTrivial p is not composite and thereby enforces that:
+-- * p is a fortiori NonZero and NonUnit
+-- * p is p-Rough, i.e. any proper divisor must be at least p, i.e. p itself
+record Prime (p : ℕ) : Set where
+  constructor prime
+  field
+    .{{nontrivial}} : NonTrivial p
+    notComposite    : ¬ Composite p
 
-¬composite⇒prime : 2 ≤ n → ¬ Composite n → Prime n
-¬composite⇒prime (s≤s (s≤s _)) ¬n-composite {d} 2≤d d<n d∣n =
-  ¬n-composite (d , 2≤d , d<n , d∣n)
+------------------------------------------------------------------------
+-- Irreducibility
 
-prime⇒¬composite : Prime n → ¬ Composite n
-prime⇒¬composite {n@(suc (suc _))} n-prime (d , 2≤d , d<n , d∣n) =
-  n-prime 2≤d d<n d∣n
+Irreducible : Pred ℕ _
+Irreducible n = ∀ {d} → d ∣ n → d ≡ 1 ⊎ d ≡ n
+
+------------------------------------------------------------------------
+-- Properties
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+-- Roughness
+
+-- 1 is always n-rough
+rough-1 : ∀ n → n Rough 1
+rough-1 _ (hasNonTrivialDivisor _ d∣1) =
+  contradiction (∣1⇒≡1 d∣1) nonTrivial⇒≢1
+
+-- Any number is 0-, 1- and 2-rough,
+-- because no proper divisor d can be strictly less than 0, 1, or 2
+0-rough : 0 Rough n
+0-rough (hasNonTrivialDivisor () _)
 
--- note that this has to recompute the factor!
-¬prime⇒composite : 2 ≤ n → ¬ Prime n → Composite n
-¬prime⇒composite {n} 2≤n ¬n-prime =
-  decidable-stable (composite? n) (¬n-prime ∘′ ¬composite⇒prime 2≤n)
+1-rough : 1 Rough n
+1-rough (hasNonTrivialDivisor {{()}} z<s _)
+
+2-rough : 2 Rough n
+2-rough (hasNonTrivialDivisor {{()}} (s<s z<s) _)
+
+-- If a number n > 1 is m-rough, then m ≤ n
+rough⇒≤ : .{{NonTrivial n}} → m Rough n → m ≤ n
+rough⇒≤ rough = ≮⇒≥ n≮m
+  where n≮m = λ m>n → rough (hasNonTrivialDivisor m>n ∣-refl)
+
+-- If a number n is m-rough, and m ∤ n, then n is (suc m)-rough
+∤⇒rough-suc : m ∤ n → m Rough n → (suc m) Rough n
+∤⇒rough-suc m∤n r (hasNonTrivialDivisor d<1+m d∣n)
+  with m<1+n⇒m<n∨m≡n d<1+m
+... | inj₁ d<m      = r (hasNonTrivialDivisor d<m d∣n)
+... | inj₂ d≡m@refl = contradiction d∣n m∤n
+
+-- If a number is m-rough, then so are all of its divisors
+rough∧∣⇒rough : m Rough o → n ∣ o → m Rough n
+rough∧∣⇒rough r n∣o bntd = r (hasNonTrivialDivisor-∣ bntd n∣o)
 
 ------------------------------------------------------------------------
--- Euclid's lemma
+-- Compositeness
+
+-- Smart constructors
+
+composite-≢ : ∀ d → .{{NonTrivial d}} → .{{NonZero n}} →
+              d ≢ n → d ∣ n → Composite n
+composite-≢ d = hasNonTrivialDivisor-≢ {d}
+
+composite-∣ : .{{NonZero n}} → Composite m → m ∣ n → Composite n
+composite-∣ (composite {d} d<m d∣n) m∣n@(divides-refl q)
+  = composite (*-monoʳ-< q d<m) (*-monoʳ-∣ q d∣n)
+  where instance
+    _ = m≢0∧n>1⇒m*n>1 q d
+    _ = m*n≢0⇒m≢0 q
+
+-- Basic (counter-)examples of Composite
+
+¬composite[0] : ¬ Composite 0
+¬composite[0] = 0-rough
+
+¬composite[1] : ¬ Composite 1
+¬composite[1] = 1-rough
+
+composite[4] : Composite 4
+composite[4] = composite-≢ 2 (λ()) (divides-refl 2)
+
+composite[6] : Composite 6
+composite[6] = composite-≢ 3 (λ()) (divides-refl 2)
+
+composite⇒nonZero : Composite n → NonZero n
+composite⇒nonZero {suc _} _ = _
+
+composite⇒nonTrivial : Composite n → NonTrivial n
+composite⇒nonTrivial {1}    composite[1] =
+  contradiction composite[1] ¬composite[1]
+composite⇒nonTrivial {2+ _} _            = _
+
+composite? : Decidable Composite
+composite? n = Dec.map CompositeUpTo⇔Composite (compositeUpTo? n)
+  where
+  -- For technical reasons, in order to be able to prove decidability
+  -- via the `all?` and `any?` combinators for *bounded* predicates on
+  -- `ℕ`, we further define the bounded counterparts to predicates
+  -- `P...` as `P...UpTo` and show the equivalence of the two.
+
+  -- Equivalent bounded predicate definition
+  CompositeUpTo : Pred ℕ _
+  CompositeUpTo n = ∃[ d ] d < n × NonTrivial d × d ∣ n
+
+  -- Proof of equivalence
+  comp-upto⇒comp : CompositeUpTo n → Composite n
+  comp-upto⇒comp (_ , d<n , ntd , d∣n) = composite d<n d∣n
+    where instance _ = ntd
+
+  comp⇒comp-upto : Composite n → CompositeUpTo n
+  comp⇒comp-upto (composite d<n d∣n) = _ , d<n , recompute-nonTrivial , d∣n
+
+  CompositeUpTo⇔Composite : CompositeUpTo n ⇔ Composite n
+  CompositeUpTo⇔Composite = mk⇔ comp-upto⇒comp comp⇒comp-upto
+
+  -- Proof of decidability
+  compositeUpTo? : Decidable CompositeUpTo
+  compositeUpTo? n = anyUpTo? (λ d → nonTrivial? d ×-dec d ∣? n) n
+
+------------------------------------------------------------------------
+-- Primality
+
+-- Basic (counter-)examples
 
--- For p prime, if p ∣ m * n, then either p ∣ m or p ∣ n.
+¬prime[0] : ¬ Prime 0
+¬prime[0] ()
+
+¬prime[1] : ¬ Prime 1
+¬prime[1] ()
+
+prime[2] : Prime 2
+prime[2] = prime 2-rough
+
+prime⇒nonZero : Prime p → NonZero p
+prime⇒nonZero _ = nonTrivial⇒nonZero _
+
+prime⇒nonTrivial : Prime p → NonTrivial p
+prime⇒nonTrivial _ = recompute-nonTrivial
+
+prime? : Decidable Prime
+prime? 0        = no ¬prime[0]
+prime? 1        = no ¬prime[1]
+prime? n@(2+ _) = Dec.map PrimeUpTo⇔Prime (primeUpTo? n)
+  where
+  -- Equivalent bounded predicate definition
+  PrimeUpTo : Pred ℕ _
+  PrimeUpTo n = ∀ {d} → d < n → NonTrivial d → d ∤ n
+
+  -- Proof of equivalence
+  prime⇒prime-upto : Prime n → PrimeUpTo n
+  prime⇒prime-upto (prime p) {d} d<n ntd d∣n
+    = p (composite d<n d∣n) where instance _ = ntd
+
+  prime-upto⇒prime : .{{NonTrivial n}} → PrimeUpTo n → Prime n
+  prime-upto⇒prime upto = prime
+    λ (composite d<n d∣n) → upto d<n recompute-nonTrivial d∣n
+
+  PrimeUpTo⇔Prime : .{{NonTrivial n}} → PrimeUpTo n ⇔ Prime n
+  PrimeUpTo⇔Prime = mk⇔ prime-upto⇒prime prime⇒prime-upto
+
+  -- Proof of decidability
+  primeUpTo? : Decidable PrimeUpTo
+  primeUpTo? n = allUpTo? (λ d → nonTrivial? d →-dec ¬? (d ∣? n)) n
+
+-- Euclid's lemma - for p prime, if p ∣ m * n, then either p ∣ m or p ∣ n.
+--
 -- This demonstrates that the usual definition of prime numbers matches
 -- the ring theoretic definition of a prime element of the semiring ℕ.
 -- This is useful for proving many other theorems involving prime numbers.
 euclidsLemma : ∀ m n {p} → Prime p → p ∣ m * n → p ∣ m ⊎ p ∣ n
-euclidsLemma m n {p@(suc (suc _))} p-prime p∣m*n = result
+euclidsLemma m n {p} pp@(prime pr) p∣m*n = result
   where
   open ∣-Reasoning
+  instance _ = prime⇒nonZero pp
 
   p∣rmn : ∀ r → p ∣ r * m * n
   p∣rmn r = begin
@@ -105,10 +258,12 @@ euclidsLemma m n {p@(suc (suc _))} p-prime p∣m*n = result
   result : p ∣ m ⊎ p ∣ n
   result with Bézout.lemma m p
   -- if the GCD of m and p is zero then p must be zero, which is
-  -- impossible as p is a prime
-  ... | Bézout.result 0 g _ = contradiction (0∣⇒≡0 (GCD.gcd∣n g)) λ()
+  -- impossible as p is a prime.
+  -- note: this should be a typechecker-rejectable case!?
+  ... | Bézout.result 0 g _ =
+    contradiction (0∣⇒≡0 (GCD.gcd∣n g)) (≢-nonZero⁻¹ _)
 
-  -- if the GCD of m and p is one then m and p is coprime, and we know
+  -- if the GCD of m and p is one then m and p are coprime, and we know
   -- that for some integers s and r, sm + rp = 1. We can use this fact
   -- to determine that p divides n
   ... | Bézout.result 1 _ (Bézout.+- r s 1+sp≡rm) =
@@ -125,19 +280,123 @@ euclidsLemma m n {p@(suc (suc _))} p-prime p∣m*n = result
       n + r * m * n ≡⟨ +-comm n (r * m * n) ⟩
       r * m * n + n ∎))
 
-  -- if the GCD of m and p is greater than one, then it must be p and hence p ∣ m.
-  ... | Bézout.result d@(suc (suc _)) g _ with d ≟ p
-  ...   | yes refl = inj₁ (GCD.gcd∣m g)
-  ...   | no  d≢p  = contradiction (GCD.gcd∣n g) (p-prime 2≤d d<p)
-    where 2≤d = s≤s (s≤s z≤n); d<p = flip ≤∧≢⇒< d≢p (∣⇒≤ (GCD.gcd∣n g))
+  -- if the GCD of m and p is greater than one, then it must be p and
+  -- hence p ∣ m.
+  ... | Bézout.result d@(2+ _) g _ with d ≟ p
+  ...   | yes d≡p@refl = inj₁ (GCD.gcd∣m g)
+  ...   | no  d≢p = contradiction (composite-≢ d d≢p (GCD.gcd∣n g)) pr
+
+-- Relationship between roughness and primality.
+prime⇒rough : Prime p → p Rough p
+prime⇒rough (prime pr) = pr
+
+-- If a number n is p-rough, and p > 1 divides n, then p must be prime
+rough∧∣⇒prime : .{{NonTrivial p}} → p Rough n → p ∣ n → Prime p
+rough∧∣⇒prime r p∣n = prime (rough∧∣⇒rough r p∣n)
+
+-- Relationship between compositeness and primality.
+composite⇒¬prime : Composite n → ¬ Prime n
+composite⇒¬prime composite[d] (prime p) = p composite[d]
+
+¬composite⇒prime : .{{NonTrivial n}} → ¬ Composite n → Prime n
+¬composite⇒prime = prime
+
+prime⇒¬composite : Prime n → ¬ Composite n
+prime⇒¬composite (prime p) = p
+
+-- Note that this has to recompute the factor!
+¬prime⇒composite : .{{NonTrivial n}} → ¬ Prime n → Composite n
+¬prime⇒composite {n} ¬prime[n] =
+  decidable-stable (composite? n) (¬prime[n] ∘′ ¬composite⇒prime)
+
+------------------------------------------------------------------------
+-- Basic (counter-)examples of Irreducible
+
+¬irreducible[0] : ¬ Irreducible 0
+¬irreducible[0] irr[0] = contradiction₂ 2≡1⊎2≡0 (λ ()) (λ ())
+  where 2≡1⊎2≡0 = irr[0] {2} (divides-refl 0)
+
+irreducible[1] : Irreducible 1
+irreducible[1] m|1 = inj₁ (∣1⇒≡1 m|1)
+
+irreducible[2] : Irreducible 2
+irreducible[2] {zero}  0∣2 with () ← 0∣⇒≡0 0∣2
+irreducible[2] {suc _} d∣2 with ∣⇒≤ d∣2
+... | z<s     = inj₁ refl
+... | s<s z<s = inj₂ refl
+
+irreducible⇒nonZero : Irreducible n → NonZero n
+irreducible⇒nonZero {zero}    = flip contradiction ¬irreducible[0]
+irreducible⇒nonZero {suc _} _ = _
+
+irreducible? : Decidable Irreducible
+irreducible? zero      = no ¬irreducible[0]
+irreducible? n@(suc _) =
+  Dec.map IrreducibleUpTo⇔Irreducible (irreducibleUpTo? n)
+  where
+  -- Equivalent bounded predicate definition
+  IrreducibleUpTo : Pred ℕ _
+  IrreducibleUpTo n = ∀ {d} → d < n → d ∣ n → d ≡ 1 ⊎ d ≡ n
+
+  -- Proof of equivalence
+  irr-upto⇒irr : .{{NonZero n}} → IrreducibleUpTo n → Irreducible n
+  irr-upto⇒irr irr-upto m∣n
+    = [ flip irr-upto m∣n , inj₂ ]′ (m≤n⇒m<n∨m≡n (∣⇒≤ m∣n))
+
+  irr⇒irr-upto : Irreducible n → IrreducibleUpTo n
+  irr⇒irr-upto irr m<n m∣n = irr m∣n
+
+  IrreducibleUpTo⇔Irreducible : .{{NonZero n}} →
+                                 IrreducibleUpTo n ⇔ Irreducible n
+  IrreducibleUpTo⇔Irreducible = mk⇔ irr-upto⇒irr irr⇒irr-upto
+
+  -- Decidability
+  irreducibleUpTo? : Decidable IrreducibleUpTo
+  irreducibleUpTo? n = allUpTo?
+    (λ m → (m ∣? n) →-dec (m ≟ 1 ⊎-dec m ≟ n)) n
+
+-- Relationship between primality and irreducibility.
+prime⇒irreducible : Prime p → Irreducible p
+prime⇒irreducible {p} pp@(prime pr) = irr
+  where
+  instance _ = prime⇒nonZero pp
+  irr : .{{NonZero p}} → Irreducible p
+  irr {0}    0∣p = contradiction (0∣⇒≡0 0∣p) (≢-nonZero⁻¹ p)
+  irr {1}    1∣p = inj₁ refl
+  irr {2+ _} d∣p = inj₂ (≤∧≮⇒≡ (∣⇒≤ d∣p) d≮p)
+    where d≮p = λ d<p → pr (composite d<p d∣p)
+
+
+irreducible⇒prime : .{{NonTrivial p}} → Irreducible p → Prime p
+irreducible⇒prime irr = prime
+  λ (composite d<p d∣p) → [ nonTrivial⇒≢1 , (<⇒≢ d<p) ]′ (irr d∣p)
+
+------------------------------------------------------------------------
+-- Using decidability
+
+-- Once we have the above decision procedures, then instead of
+-- constructing proofs of e.g. Prime-ness by hand, we call the
+-- appropriate function, and use the witness extraction functions
+-- `from-yes`, `from-no` to return the checked proofs.
 
 private
 
-  -- Example: 2 is prime.
+  -- Example: 2 is prime, but not-composite.
   2-is-prime : Prime 2
   2-is-prime = from-yes (prime? 2)
 
+  2-is-not-composite : ¬ Composite 2
+  2-is-not-composite = from-no (composite? 2)
+
+  -- Example: 4 and 6 are composite, hence not-prime
+  4-is-composite : Composite 4
+  4-is-composite = from-yes (composite? 4)
+
+  4-is-not-prime : ¬ Prime 4
+  4-is-not-prime = from-no (prime? 4)
 
-  -- Example: 6 is composite
   6-is-composite : Composite 6
   6-is-composite = from-yes (composite? 6)
+
+  6-is-not-prime : ¬ Prime 6
+  6-is-not-prime = from-no (prime? 6)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 37b1f33ee0..9df927064a 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -60,6 +60,15 @@ nonZero? : U.Decidable NonZero
 nonZero? zero    = no NonZero.nonZero
 nonZero? (suc n) = yes _
 
+------------------------------------------------------------------------
+-- Properties of NonTrivial
+------------------------------------------------------------------------
+
+nonTrivial? : U.Decidable NonTrivial
+nonTrivial? 0      = no λ()
+nonTrivial? 1      = no λ()
+nonTrivial? (2+ n) = yes _
+
 ------------------------------------------------------------------------
 -- Properties of _≡_
 ------------------------------------------------------------------------
@@ -902,6 +911,12 @@ m*n≡0⇒m≡0∨n≡0 (suc m) {zero}  eq = inj₂ refl
 m*n≢0 : ∀ m n → .{{_ : NonZero m}} .{{_ : NonZero n}} → NonZero (m * n)
 m*n≢0 (suc m) (suc n) = _
 
+m*n≢0⇒m≢0 : ∀ m {n} → .{{NonZero (m * n)}} → NonZero m
+m*n≢0⇒m≢0 (suc _) = _
+
+m*n≢0⇒n≢0 : ∀ m {n} → .{{NonZero (m * n)}} → NonZero n
+m*n≢0⇒n≢0 m {n} rewrite *-comm m n = m*n≢0⇒m≢0 n {m}
+
 m*n≡0⇒m≡0 : ∀ m n .{{_ : NonZero n}} → m * n ≡ 0 → m ≡ 0
 m*n≡0⇒m≡0 zero (suc _) eq = refl
 
@@ -922,6 +937,12 @@ m*n≡1⇒n≡1 m n eq = m*n≡1⇒m≡1 n m (trans (*-comm n m) eq)
   (m * o) * (n * p) ∎
   where open CommSemigroupProperties *-commutativeSemigroup
 
+m≢0∧n>1⇒m*n>1 : ∀ m n .{{_ : NonZero m}} .{{_ : NonTrivial n}} → NonTrivial (m * n)
+m≢0∧n>1⇒m*n>1 (suc m) (2+ n) = _
+
+n≢0∧m>1⇒m*n>1 : ∀ m n .{{_ : NonZero n}} .{{_ : NonTrivial m}} → NonTrivial (m * n)
+n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
+
 ------------------------------------------------------------------------
 -- Other properties of _*_ and _≤_/_<_
 
@@ -1704,7 +1725,7 @@ pred-mono-≤ : pred Preserves _≤_ ⟶ _≤_
 pred-mono-≤ {zero}          _   = z≤n
 pred-mono-≤ {suc _} {suc _} m≤n = s≤s⁻¹ m≤n
 
-pred-mono-< : .⦃ _ : NonZero m ⦄ → m < n → pred m < pred n
+pred-mono-< : .{{NonZero m}} → m < n → pred m < pred n
 pred-mono-< {m = suc _} {n = suc _} = s<s⁻¹
 
 ------------------------------------------------------------------------
diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda
index 1e49894eb6..0948447163 100644
--- a/src/Data/Rational/Base.agda
+++ b/src/Data/Rational/Base.agda
@@ -16,7 +16,7 @@ open import Data.Integer.Base as ℤ
 open import Data.Nat.GCD
 open import Data.Nat.Coprimality as C
   using (Coprime; Bézout-coprime; coprime-/gcd; coprime?; ¬0-coprimeTo-2+)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc) hiding (module ℕ)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; 2+) hiding (module ℕ)
 open import Data.Rational.Unnormalised.Base as ℚᵘ using (ℚᵘ; mkℚᵘ)
 open import Data.Sum.Base using (inj₂)
 open import Function.Base using (id)
@@ -189,10 +189,11 @@ open ℤ public
 -- Constructors
 
 ≢-nonZero : ∀ {p} → p ≢ 0ℚ → NonZero p
-≢-nonZero {mkℚ -[1+ _ ] _       _} _   = _
-≢-nonZero {mkℚ +[1+ _ ] _       _} _   = _
-≢-nonZero {mkℚ +0       zero    _} p≢0 = contradiction refl p≢0
-≢-nonZero {mkℚ +0       (suc d) c} p≢0 = contradiction (λ {i} → C.recompute c {i}) ¬0-coprimeTo-2+
+≢-nonZero {mkℚ -[1+ _ ] _         _} _   = _
+≢-nonZero {mkℚ +[1+ _ ] _         _} _   = _
+≢-nonZero {mkℚ +0       zero      _} p≢0 = contradiction refl p≢0
+≢-nonZero {mkℚ +0       d@(suc m) c} p≢0 =
+  contradiction (λ {d} → C.recompute c {d}) (¬0-coprimeTo-2+ {{ℕ.nonTrivial {m}}})
 
 >-nonZero : ∀ {p} → p > 0ℚ → NonZero p
 >-nonZero {p@(mkℚ _ _ _)} (*<* p<q) = ℚᵘ.>-nonZero {toℚᵘ p} (ℚᵘ.*<* p<q)