diff --git a/Cubical/Data/Nat/Count.agda b/Cubical/Data/Nat/Count.agda
new file mode 100644
index 0000000000..45644c9a39
--- /dev/null
+++ b/Cubical/Data/Nat/Count.agda
@@ -0,0 +1,255 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Count where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum hiding (elim ; rec ; map)
+open import Cubical.Data.List hiding (elim ; rec ; map)
+
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+private
+    variable
+        ℓ ℓ' ℓ'' : Level
+
+    -- some definitions and lemmas
+
+    decToN : {A : Type ℓ} → Dec A → ℕ
+    decToN (yes _) = 1
+    decToN (no  _) = 0
+
+    data All {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ-max ℓ ℓ') where
+      []  :                             All P []
+      _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)
+
+    mapAll : {A : Type ℓ} {P Q : A → Type ℓ'} {xs : List A} → (∀ {a} → P a → Q a) → All P xs → All Q xs
+    mapAll f [] = []
+    mapAll f (Px ∷ Pxs) = f Px ∷ mapAll f Pxs
+
+    add-equations : ∀ {a} {b} {c} {d} → a ≡ b → c ≡ d → a + c ≡ b + d
+    add-equations {b = b} {c = c} a=b c=d = cong (_+ c) a=b ∙ cong (b +_) c=d
+
+    <≠ : forall {m} {n} → m < n → ¬ m ≡ n
+    <≠ {m = m} m<n m=n = <-asym m<n (0 , sym m=n)
+
+
+DecProd-aux : {A : Type ℓ} (P : A → Type ℓ') (Q : A → Type ℓ'') → ∀ {a} →
+              Dec (P a) → Dec (Q a) → Dec (P a × Q a)
+DecProd-aux _ _ (yes Pa) (yes Qa) = yes (Pa , Qa)
+DecProd-aux _ _ (yes Pa) (no ¬Qa) = no (λ pf → ¬Qa (pf .snd))
+DecProd-aux _ _ (no ¬Pa) _        = no (λ pf → ¬Pa (pf .fst))
+
+DecProd : {A : Type ℓ} {P : A → Type ℓ'} {Q : A → Type ℓ''} →
+          (∀ a → Dec (P a)) → (∀ a → Dec (Q a)) → (∀ a → Dec (P a × Q a))
+DecProd {P = P} {Q = Q} Pdec Qdec a = DecProd-aux P Q (Pdec a) (Qdec a)
+
+
+-- splitting naturals below a bound
+-- into those for which a given decidable property holds
+-- and those for which it does not
+module _ (P : ℕ → Type ℓ) (Pdec : ∀ n → Dec (P n)) where
+
+    goodSplit : ℕ → Type ℓ
+    goodSplit n = Σ[ (goods , bads) ∈ List ℕ × List ℕ ]
+                   (All P goods × All (λ n → ¬ (P n)) bads)
+                 × (All (_< n) goods × All (_< n) bads)
+                 × ((length goods) + (length bads) ≡ n)
+
+    splitBelow-aux : (n : ℕ) → goodSplit n → Dec (P n) → goodSplit (suc n)
+    splitBelow-aux n ((ws , ls) , (Pws , ¬Pls) , (ws<n , ls<n) , sum) (yes Pn) =
+        (n ∷ ws , ls) ,
+        (Pn ∷ Pws , ¬Pls) ,
+        ((0 , refl) ∷ ws<sn , ls<sn) ,
+        cong suc sum where
+            ws<sn = mapAll (λ x<n → <-trans x<n (0 , refl)) ws<n
+            ls<sn = mapAll (λ x<n → <-trans x<n (0 , refl)) ls<n
+    splitBelow-aux n ((ws , ls) , (Pws , ¬Pls) , (ws<n , ls<n) , sum) (no ¬Pn) =
+        (ws , n ∷ ls) ,
+        (Pws , ¬Pn ∷ ¬Pls) ,
+        (ws<sn , (0 , refl) ∷ ls<sn) ,
+        +-suc _ _ ∙ cong suc sum where
+            ws<sn = mapAll (λ x<n → <-trans x<n (0 , refl)) ws<n
+            ls<sn = mapAll (λ x<n → <-trans x<n (0 , refl)) ls<n
+
+    splitBelow : (top : ℕ) → goodSplit top
+    splitBelow zero = ([] , []) , ([] , []) , ([] , []) , refl
+    splitBelow (suc n) = splitBelow-aux n (splitBelow n) (Pdec n)
+
+-- definitions and properties of counting:
+-- how many naturals in a given range have a given decidable property?
+-- note: lower bound included, upper bound excluded (if equal nothing counted)
+module _ (P : ℕ → Type ℓ) (Pdec : ∀ n → Dec (P n)) where
+    countBelow : ℕ → ℕ
+    countBelow top = length ((splitBelow P Pdec top) .fst .fst)
+
+    countRange : (low top : ℕ) → low ≤ top → ℕ
+    countRange low top _ = length (splitBelow
+                           (λ n → (P n) × (low ≤ n)) (DecProd Pdec (≤Dec low)) top
+                           .fst .fst)
+
+    least→count=0 : {n : ℕ} → (∀ z → P z → n ≤ z) → countBelow n ≡ 0
+    least→count=0 {n} least = answer where
+        split = splitBelow P Pdec n
+        goods = split .fst .fst
+        Pgoods = split .snd .fst .fst
+        goods<n = split .snd .snd .fst .fst
+
+        answer : countBelow n ≡ 0
+        answer with goods | goods<n | Pgoods
+        ... | [] | [] | [] = refl
+        ... | x ∷ _ | x<n ∷ _ | Px ∷ _ = ⊥.rec (<-asym x<n (least x Px))
+
+    countRefl≡0 : (n : ℕ) → countRange n n (0 , refl) ≡ 0
+    countRefl≡0 n = answer where
+        split = splitBelow (λ x → (P x) × (n ≤ x)) (DecProd Pdec (≤Dec n)) n
+        ws = split .fst .fst
+        Pws = split .snd .fst .fst
+        ws<n = split .snd .snd .fst .fst
+
+        answer : length ws ≡ 0
+        answer with ws | Pws | ws<n
+        ... | [] | [] | [] = refl
+        ... | _ | (_ , n≤w) ∷ _ | w<n ∷ _ = ⊥.rec (<-asym w<n n≤w)
+
+    countRangeSuc : (l t : ℕ) → (l≤t : l ≤ t) →
+                    (DPt : Dec (P t)) → (DPt ≡ Pdec t) →
+                    (decToN DPt) + countRange l t l≤t ≡ countRange l (suc t) (≤-suc l≤t)
+    countRangeSuc l t l≤t (yes Pt) p = answer where
+        Q = λ n → (P n) × (l ≤ n)
+        dprod = λ a → DecProd-aux P (l ≤_) (Pdec a) (≤Dec l a)
+        IH = splitBelow Q dprod t
+
+        replace : Σ[ Qt ∈ Q t ] yes Qt ≡ dprod t
+        replace with dprod t
+        ... | no ¬Qt = ⊥.rec (¬Qt (Pt , l≤t))
+        ... | yes Qt = Qt , refl
+
+        answer : suc (length (IH .fst .fst))
+                 ≡ length (splitBelow-aux Q dprod t IH (dprod t) .fst .fst)
+        answer = cong (λ x → length (splitBelow-aux Q dprod t IH x .fst .fst)) (replace .snd)
+
+    countRangeSuc l t l≤t (no ¬Pt) p = answer where
+        Q = λ n → (P n) × (l ≤ n)
+        dprod = λ a → DecProd-aux P (l ≤_) (Pdec a) (≤Dec l a)
+        IH = splitBelow Q dprod t
+
+        replace : Σ[ ¬Qt ∈ ¬ (Q t) ] no ¬Qt ≡ dprod t
+        replace with dprod t
+        ... | no ¬Qt = ¬Qt , refl
+        ... | yes (Pt , _) = ⊥.rec (¬Pt Pt)
+
+        answer : length (IH .fst .fst)
+                 ≡ length (splitBelow-aux Q dprod t IH (dprod t) .fst .fst)
+        answer = cong (λ x → length (splitBelow-aux Q dprod t IH x .fst .fst)) (replace .snd)
+
+    countBelowSuc : (n : ℕ) → (DPn : Dec (P n)) → (DPn ≡ Pdec n) →
+                    (decToN DPn) + countBelow n ≡ countBelow (suc n)
+    countBelowSuc n (yes Pn) p =
+        cong (λ x → length (splitBelow-aux P Pdec n (splitBelow P Pdec n) x .fst .fst)) p
+    countBelowSuc n (no ¬Pn) p =
+        cong (λ x → length (splitBelow-aux P Pdec n (splitBelow P Pdec n) x .fst .fst)) p
+
+
+    countWorks-aux : (l t : ℕ) → (l≤st : l ≤ (suc t)) →
+                     ((l≤t : l ≤ t) → (countRange l t l≤t) + (countBelow l) ≡ countBelow t) →
+                     ((l < suc t) ⊎ (l ≡ suc t)) →
+                     (countRange l (suc t) l≤st) + (countBelow l) ≡ countBelow (suc t)
+    countWorks-aux l t l≤st recf (inr l=st) = (cong (_+ countBelow l) p2 ∙ p1) ∙ p3 where
+        p1 : countRange l l (0 , refl) + countBelow l ≡ countBelow l
+        p1 = cong (_+ countBelow l) (countRefl≡0 l)
+        p2 : countRange l (suc t) l≤st ≡ countRange l l (0 , refl)
+        p2 = sym (cong₂ (λ x l≤x → countRange l x l≤x)
+                        l=st
+                        (isProp→PathP (λ i → isProp≤) (0 , refl) l≤st))
+        p3 : countBelow l ≡ countBelow (suc t)
+        p3 = cong (countBelow) l=st
+
+    countWorks-aux l t l≤st recf (inl l<st) = induct (recf l≤t) where
+        l≤t : l ≤ t
+        l≤t = pred-≤-pred l<st
+        induct : (countRange l t l≤t) + (countBelow l) ≡ countBelow t →
+                 (countRange l (suc t) l≤st) + (countBelow l) ≡ countBelow (suc t)
+        induct IH = sym (cong (_+ countBelow l) p1) ∙ p3 ∙ p2 where
+            p1 : decToN (Pdec t) + countRange l t l≤t ≡ countRange l (suc t) l≤st
+            p1 = countRangeSuc l t l≤t (Pdec t) refl
+            p2 : decToN (Pdec t) + countBelow t ≡ countBelow (suc t)
+            p2 = countBelowSuc t (Pdec t) refl
+            p3 : decToN (Pdec t) + countRange l t l≤t + countBelow l ≡
+                    decToN (Pdec t) + countBelow t
+            p3 = sym (+-assoc (decToN (Pdec t)) (countRange l t l≤t) (countBelow l))
+                    ∙ cong (decToN (Pdec t) +_) IH
+
+    countWorks : (low top : ℕ) → (l≤t : low ≤ top) →
+                 (countRange low top l≤t) + (countBelow low) ≡ countBelow top
+    countWorks l zero l≤0 = cong (λ x → countBelow x) (≤0→≡0 l≤0)
+    countWorks l (suc t) l≤st = countWorks-aux l t l≤st (countWorks l t) (≤-split l≤st)
+
+
+    leastAboveLow-aux : (l t : ℕ) → (l<st : l < (suc t)) →
+                        (Pl : P l) → (Pdec l ≡ yes Pl) → (∀ z → (l < z) × (P z) → (suc t) ≤ z) →
+                        (l < t) ⊎ (l ≡ t) →
+                        (l < t → countRange l t (pred-≤-pred l<st) ≡ 1) →
+                        countRange l (suc t) (<-weaken l<st) ≡ 1
+    leastAboveLow-aux l t l<st Pl p least (inr l=t) _ =
+        sym (countRangeSuc l t (0 , l=t) (Pdec t) refl) ∙ p3 where
+            p1 : decToN (Pdec t) ≡ 1
+            p1 = cong (λ x → decToN (Pdec x)) (sym l=t) ∙ cong decToN p
+            p2 : countRange l t (0 , l=t) ≡ 0
+            p2 = cong₂ (λ x l≤x → countRange l x l≤x)
+                       (sym l=t)
+                       (isProp→PathP (λ i → isProp≤) (0 , l=t) (0 , refl))
+                 ∙ countRefl≡0 l
+            p3 : decToN (Pdec t) + countRange l t (0 , l=t) ≡ 1
+            p3 = add-equations p1 p2
+    leastAboveLow-aux l t l<st Pl p least (inl l<t) recf =
+        p2 ∙ cong (_+ countRange l t (pred-≤-pred l<st)) p1 ∙ IH where
+            IH : countRange l t (pred-≤-pred l<st) ≡ 1
+            IH = recf l<t
+            p1 : decToN (Pdec t) ≡ 0
+            p1 with Pdec t
+            ... | no   _ = refl
+            ... | yes Pt = ⊥.rec (<-asym (least t (l<t , Pt)) (0 , refl))
+            p2 : countRange l (suc t) (<-weaken l<st)
+                 ≡ (decToN (Pdec t)) + countRange l t (pred-≤-pred l<st)
+            p2 = sym (countRangeSuc l t (pred-≤-pred l<st) (Pdec t) refl)
+
+    leastAboveLow : (l t : ℕ) → (Pl : P l) → (Pdec l ≡ yes Pl) →
+                    (∀ z → (l < z) × (P z) → t ≤ z) → (l<t : l < t) →
+                    countRange l t (<-weaken l<t) ≡ 1
+    leastAboveLow _ zero _ _ _ l<0 = ⊥.rec (¬-<-zero l<0)
+    leastAboveLow l (suc t) Pl p least l<st =
+        leastAboveLow-aux l t l<st Pl p least (<-split l<st)
+                          (leastAboveLow l t Pl p (λ z Qz → <-weaken (least z Qz)))
+
+
+    countBelow-lt-aux : (x y : ℕ) → (Px : P x) → (Pdec x ≡ yes Px) →
+                        x < (suc y) → (x < y) ⊎ (x ≡ y) →
+                        (x < y → countBelow x < countBelow y) →
+                        countBelow x < countBelow (suc y)
+    countBelow-lt-aux x _ Px p _ (inr x=y) _ = 0 , q ∙ cong (countBelow ∘ suc) x=y where
+        q : suc (countBelow x) ≡ countBelow (suc x)
+        q = countBelowSuc x (yes Px) (sym p)
+    countBelow-lt-aux x y Px p x<sy (inl x<y) recf =
+        <≤-trans (recf x<y) (decToN (Pdec y) , countBelowSuc y (Pdec y) refl)
+
+    countBelow-lt : (x y : ℕ) →
+                    (Px : P x) → (Pdec x ≡ yes Px) →
+                    x < y → countBelow x < countBelow y
+    countBelow-lt _ zero _ _ x<0 = ⊥.rec (¬-<-zero x<0)
+    countBelow-lt x (suc y) Px p x<sy =
+        countBelow-lt-aux x y Px p x<sy
+        (<-split x<sy) (countBelow-lt x y Px p)
+
+    countBelowYesInj : (x y : ℕ) →  (Px : P x) → (Py : P y) →
+                       (Pdec x ≡ yes Px) → (Pdec y ≡ yes Py) →
+                       countBelow x ≡ countBelow y → x ≡ y
+    countBelowYesInj x y Px Py q1 q2 p with x ≟ y
+    ... | eq x=y = x=y
+    ... | lt x<y = ⊥.rec (<≠ (countBelow-lt x y Px q1 x<y) p)
+    ... | gt y<x = ⊥.rec (<≠ (countBelow-lt y x Py q2 y<x) (sym p))
diff --git a/Cubical/Data/Nat/Primes/Base.agda b/Cubical/Data/Nat/Primes/Base.agda
new file mode 100644
index 0000000000..895e3324e9
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Base.agda
@@ -0,0 +1,31 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Base where
+
+open import Cubical.Foundations.Prelude public
+open import Cubical.Data.Nat
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Divisibility
+open import Cubical.Data.Sum hiding (elim ; rec ; map)
+open import Cubical.Data.Nat.Primes.Lemmas using (1<·1<=3<)
+
+
+record isPrime (n : ℕ) : Type where
+    no-eta-equality
+    constructor prime
+    field
+        n-proper : 1 < n
+        primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)
+
+record isComposite (n : ℕ) : Type where
+    no-eta-equality
+    constructor composite
+    field
+        p q : ℕ
+        p-prime  : isPrime p
+        q-proper : 1 < q
+        factors : p · q ≡ n
+        least : ∀ z → 1 < z → z ∣ n → p ≤ z
+
+    3<n : 3 < n
+    3<n = subst (λ x → 3 < x) factors (1<·1<=3< (isPrime.n-proper p-prime) q-proper)
diff --git a/Cubical/Data/Nat/Primes/Concrete.agda b/Cubical/Data/Nat/Primes/Concrete.agda
new file mode 100644
index 0000000000..ef2f3c8719
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Concrete.agda
@@ -0,0 +1,52 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Concrete where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+prime2 : isPrime 2
+prime2 = prime (0 , refl) primality-2 where
+    primality-2 : (d : ℕ) → d ∣ 2 → (d ≡ 1) ⊎ (d ≡ 2)
+    primality-2 d d∣2 with (≤-split (m∣n→m≤n snotz d∣2))
+    ... | inr d=2 = inr d=2
+    ... | inl d<2 with <-split d<2
+    ... | inr d=1 = inl d=1
+    ... | inl d<1 = ⊥.rec (¬<1∣sn d 1 d<1 d∣2)
+
+
+private
+
+    -- can be used to directly prove primality of a specific number
+    notDiv : ∀ d n → Σ[ k ∈ ℕ ] (k · d < n) × (n < suc k · d) → ¬ d ∣ n
+    notDiv d n (k , kd<n , n<d+kd) d∣n-trunc
+        with d | (∣-untrunc d∣n-trunc) | (fst (∣-untrunc d∣n-trunc) ≟ k)
+    ...       | d | (c , cd=n) | (eq c=k) = <≠ kd<n (subst (λ x → x · d ≡ n) c=k cd=n)
+    ...       | 0 | (c , cd=n) | (lt c<k) = ¬-<-zero (subst (λ x → k · 0 < x)
+                                                            (sym (cd=n) ∙ sym (0≡m·0 c))
+                                                            kd<n)
+    ... | suc d-1 | (c , cd=n) | (lt c<k) = <≠ (lem1 c k d-1 n c<k kd<n) cd=n
+    ...       | d | (0 , cd=n) | (gt k<c) = ¬-<-zero k<c
+    ... | d | (suc c , d+cd=n) | (gt k<sc) with (<-split k<sc)
+    ...                        | inr k=c = <≠ n<d+kd
+                                           (sym (subst (λ x → d + x · d ≡ n) (sym k=c) d+cd=n))
+    ...                        | inl k<c = <≠ (lem2 c k d n k<c n<d+kd) (sym d+cd=n)
+
+    -- example
+    prime5 : isPrime 5
+    prime5 = prime (3 , refl) primality-5 where
+        primality-5 : (d : ℕ) → d ∣ 5 → (d ≡ 1) ⊎ (d ≡ 5)
+        primality-5 d d∣5 with (≤-split (m∣n→m≤n snotz d∣5))
+        ... | inr d=5 = inr d=5
+        ... | inl d<5 with <-split d<5
+        ... | inr d=4 = ⊥.rec (notDiv 4 5 (1 , (0 , refl) , (2 , refl)) (subst (λ x → x ∣ 5) d=4 d∣5))
+        ... | inl d<4 with <-split d<4
+        ... | inr d=3 = ⊥.rec (notDiv 3 5 (1 , (1 , refl) , (0 , refl)) (subst (λ x → x ∣ 5) d=3 d∣5))
+        ... | inl d<3 with <-split d<3
+        ... | inr d=2 = ⊥.rec (notDiv 2 5 (2 , (0 , refl) , (0 , refl)) (subst (λ x → x ∣ 5) d=2 d∣5))
+        ... | inl d<2 with <-split d<2
+        ... | inr d=1 = inl d=1
+        ... | inl d<1 = ⊥.rec (¬<1∣sn d 4 d<1 d∣5)
diff --git a/Cubical/Data/Nat/Primes/DecProps.agda b/Cubical/Data/Nat/Primes/DecProps.agda
new file mode 100644
index 0000000000..d957eb1ee9
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/DecProps.agda
@@ -0,0 +1,116 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.DecProps where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Nat.Primes.Factors
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+open import Cubical.Data.Sum.Properties
+open import Cubical.Reflection.RecordEquiv
+
+open isPrime
+open isComposite
+
+
+private
+    variable
+        ℓ ℓ' : Level
+
+    funcProp : {A : Type ℓ} {B : A → Type ℓ'} → (∀ a → isProp (B a)) → isProp (∀ a → B a)
+    funcProp BProp f g = funExt (λ x → BProp x (f x) (g x))
+
+    PropIso : ∀ {A : Type ℓ} {B : Type ℓ'} → isProp A → isProp B → (A → B) → (B → A) → Iso A B
+    PropIso propA propB fun inv = iso fun inv (λ _ → propB _ _) (λ _ → propA _ _)
+
+
+primeProp : ∀ n → isProp (isPrime n)
+primeProp n np np' i .n-proper = isProp≤ (np .n-proper) (np' .n-proper) i
+primeProp n np np' i .primality =
+    (funcProp  (λ x → funcProp  (λ x∣n →
+    isProp⊎ (isSetℕ x 1) (isSetℕ x n)
+    λ x=1 x=n → ¬n<n (subst (λ y → y < n) (sym x=1 ∙ x=n) (np .n-proper))))
+    (np .primality) (np' .primality)) i
+
+compProp : ∀ n → isProp (isComposite n)
+compProp n nc nc' = answer where
+    p1 = nc .p
+    p2 = nc' .p
+    q1 = nc .q
+    q2 = nc' .q
+    pp1 = nc .p-prime
+    pp2 = nc' .p-prime
+    1<p1 = pp1 .n-proper
+    1<p2 = pp2 .n-proper
+    1<q1 = nc .q-proper
+    1<q2 = nc' .q-proper
+    pq=n = nc .factors
+    pq=n' = nc' .factors
+    least1 = nc .least
+    least2 = nc' .least
+
+    p1∣n = ∣ (q1 , ·-comm q1 p1 ∙ pq=n) ∣₁
+    p2∣n = ∣ (q2 , ·-comm q2 p2 ∙ pq=n') ∣₁
+
+    p1=p2 : p1 ≡ p2
+    p1=p2 = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n)
+
+    q1=q2 : q1 ≡ q2
+    q1=q2 = inj-·0< q1 q2 (<-weaken 1<p1) (pq=n ∙ sym (subst (λ x → x · q2 ≡ n) (sym p1=p2) pq=n'))
+
+    leastProp : ∀ x → isProp ((p2' : ℕ) → 1 < p2' → p2' ∣ n → x ≤ p2')
+    leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
+
+    answer : nc ≡ nc'
+    answer i .p = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n) i
+    answer i .q = q1=q2 i
+    answer i .p-prime = isProp→PathP (λ j → primeProp (p1=p2 j)) pp1 pp2 i
+    answer i .q-proper = isProp→PathP (λ j → isProp≤ {n = q1=q2 j}) 1<q1 1<q2 i
+    answer i .factors = isProp→PathP (λ j → isSetℕ (p1=p2 j · q1=q2 j) n) pq=n pq=n' i
+    answer i .least = isProp→PathP (λ j → leastProp (p1=p2 j)) least1 least2 i
+
+
+prime→¬comp : ∀ n → isPrime n → ¬ isComposite n
+prime→¬comp n pn cn with (pn .primality) (cn .q) (∣ (cn .p , cn .factors) ∣₁)
+... | inl q=1 = <≠ (cn .q-proper) (sym q=1)
+... | inr q=n = <≠ (PropFac< qfac pfac n (n-proper pp) (<-weaken (pn .n-proper)) (·-comm qfac pfac ∙ pq=n)) q=n where
+        pfac = cn .p
+        pp = cn .p-prime
+        qfac = cn .q
+        pq=n = cn .factors
+
+¬comp→prime : ∀ n → 1 < n → ¬ isComposite n → isPrime n
+¬comp→prime n 1<n ¬nc with primeOrComp n 1<n
+... | inl np = np
+... | inr nc = ⊥.rec (¬nc nc)
+
+comp→¬prime : ∀ n → isComposite n → ¬ isPrime n
+comp→¬prime n nc np = prime→¬comp n np nc
+
+¬prime→comp : ∀ n → 1 < n → ¬ isPrime n → isComposite n
+¬prime→comp n 1<n ¬np with primeOrComp n 1<n
+... | inr nc = nc
+... | inl np = ⊥.rec (¬np np)
+
+prime≡¬comp : ∀ n → 1 < n → (isPrime n) ≡ (¬ isComposite n)
+prime≡¬comp n 1<n =
+    isoToPath (PropIso (primeProp n) (isProp¬ (isComposite n)) (prime→¬comp n) (¬comp→prime n 1<n))
+
+comp≡¬prime : ∀ n → 1 < n → (isComposite n) ≡ (¬ isPrime n)
+comp≡¬prime n 1<n =
+    isoToPath (PropIso (compProp n) (isProp¬ (isPrime n)) (comp→¬prime n) (¬prime→comp n 1<n))
+
+DecPrime : ∀ n → Dec (isPrime n)
+DecPrime 0 = no λ 0p → ¬-<-zero (0p .n-proper)
+DecPrime 1 = no λ 1p → ¬n<n (1p .n-proper)
+DecPrime n@(suc (suc n-2)) with (primeOrComp n (n-2 , +-comm n-2 2))
+... | inl np = yes np
+... | inr nc = no (comp→¬prime n nc)
+
+DecComp : ∀ n → Dec (isComposite n)
+DecComp 0 = no λ 0c → ¬n<n (<-trans (2 , refl) (isComposite.3<n 0c))
+DecComp 1 = no λ 1c → ¬n<n (<-trans (1 , refl) (isComposite.3<n 1c))
+DecComp n@(suc (suc n-2)) with (primeOrComp n (n-2 , +-comm n-2 2))
+... | inr nc = yes nc
+... | inl np = no (prime→¬comp n np)
diff --git a/Cubical/Data/Nat/Primes/Factors.agda b/Cubical/Data/Nat/Primes/Factors.agda
new file mode 100644
index 0000000000..ed66a64f6a
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Factors.agda
@@ -0,0 +1,118 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Factors where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+leastFactorIsPrime : ∀ n p → HasFactor n p → (∀ d → HasFactor n d → p ≤ d) → isPrime p
+leastFactorIsPrime _ 0 (1<p , _) _ = ⊥.rec (¬-<-zero 1<p)
+leastFactorIsPrime n p@(suc p-1) (1<p , p∣n) least = prime 1<p primality where
+    primality : ∀ (d : ℕ) → d ∣ p → (d ≡ 1) ⊎ (d ≡ p)
+    primality zero d∣p = ⊥.rec (¬z∣sn p-1 d∣p)
+    primality d@(suc d-1) d∣p with ≤-split (m∣n→m≤n snotz d∣p)
+    ... | inr d=p = inr d=p
+    ... | inl d<p with (d ≟ 1)
+    ... | eq d=1 = inl d=1
+    ... | lt d<1 = ⊥.rec (¬s<1 d<1)
+    ... | gt 1<d = ⊥.rec (<-asym d<p (least d (1<d , ∣-trans d∣p p∣n)))
+
+
+primeOrComp : ∀ n → 1 < n → (isPrime n) ⊎ (isComposite n)
+primeOrComp zero 1<0 = ⊥.rec (¬-<-zero 1<0)
+primeOrComp n@(suc n-1) 1<n = answer where
+
+    LF : Σ[ p ∈ ℕ ] (HasFactor n p) × (∀ z → (HasFactor n z) → p ≤ z)
+    LF = findLeast (1<n , ∣-refl refl) DecHF
+
+    p = LF .fst
+    HFnp = LF .snd .fst
+    1<p = HFnp .fst
+    p∣n = ∣-untrunc (HFnp .snd)
+    q = p∣n .fst
+    p≤n = m∣n→m≤n snotz (HFnp .snd)
+    pq=n = ·-comm p q ∙ p∣n .snd
+
+    p-least : ∀ z → (HasFactor n z) → p ≤ z
+    p-least = LF .snd .snd
+
+    p-prime : isPrime p
+    p-prime = leastFactorIsPrime n p HFnp p-least
+
+    answer : (isPrime n) ⊎ (isComposite n)
+    answer with (Dichotomyℕ n p)
+    ... | inl n≤p = inl (subst (λ x → isPrime x) (≤-antisym p≤n n≤p) p-prime)
+    ... | inr p<n = inr (composite p q p-prime 1<q pq=n (λ z 1<z z∣n → p-least z (1<z , z∣n)))
+            where
+                1<q : 1 < q
+                1<q with (1 ≟ q)
+                ... | lt 1<q = 1<q
+                ... | gt q<1 = ⊥.rec (1<→¬=0 n 1<n
+                                     (sym pq=n ∙ cong (p ·_) (<1→0 q q<1) ∙ sym (0≡m·0 p)))
+                ... | eq 1=q = ⊥.rec (¬n<n (subst (λ x → x < n)
+                                                  (subst
+                                                        (λ x → p ≡ p · x)
+                                                        1=q
+                                                        (sym (·-identityʳ p)) ∙ pq=n)
+                                                  p<n))
+
+open isPrime
+open isComposite
+
+newPrime : ∀ n → Σ[ p ∈ ℕ ] (n < p) × (isPrime p)
+newPrime n with primeOrComp (suc (factorial n)) (suc< (0<factorial n))
+... | inl sfnp = (suc (factorial n)) , suc-≤-suc (n≤! n) , sfnp
+... | inr cn with Dichotomyℕ (cn .p) n
+... | inr n<p = (cn .p) , n<p , (cn .p-prime)
+... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 (cn .p) p∣1))) where
+        1<p = cn .p-prime .n-proper
+        p∣1 : (cn .p) ∣ 1
+        p∣1 = ∣+-cancel (cn .p) 1 (n !) (≤n∣n! (cn .p) n p≤n (1<→¬=0 (cn .p) 1<p)) (∣ (cn .q) , ·-comm (cn .q) (cn .p) ∙ (cn .factors) ∣₁)
+
+
+record PrimeFactors (n : ℕ) : Type where
+    no-eta-equality
+    constructor pfs
+    field
+        primes : List ℕ
+        factored : product primes ≡ n
+        allPrime : All isPrime primes
+open PrimeFactors
+
+PF-prime : ∀ n → isPrime n → PrimeFactors n
+PF-prime n np = pfs (n ∷ []) (·-identityʳ n) (np ∷ [])
+
+PF-comp-work : ∀ n → (∀ m → m < n → isComposite m → PrimeFactors m) → isComposite n →
+               PrimeFactors n
+PF-comp-work n rec nComp =
+    pfs (pfac ∷ primes qFacs)
+        (subst (λ x → pfac · x ≡ n) (sym (factored qFacs)) pq=n)
+        (pp ∷ allPrime qFacs)
+        where
+            pfac = nComp .p
+            qfac = nComp .q
+            pp = nComp .p-prime
+            1<q = nComp .q-proper
+            pq=n = nComp .factors
+
+            qFacs : PrimeFactors qfac
+            qFacs with (primeOrComp qfac 1<q)
+            ... | inl qp = PF-prime qfac qp
+            ... | inr qc = rec qfac (PropFac< qfac pfac n 1<p 0<n (·-comm qfac pfac ∙ pq=n)) qc where
+                    1<p = isPrime.n-proper pp
+                    0<n = <-trans (2 , refl) (isComposite.3<n nComp)
+
+PF-comp : ∀ n → isComposite n → PrimeFactors n
+PF-comp = WFI.induction <-wellfounded PF-comp-work
+
+PF-aux : ∀ n → (isPrime n) ⊎ (isComposite n) → PrimeFactors n
+PF-aux n (inl np) = PF-prime n np
+PF-aux n (inr nc) = PF-comp n nc
+
+factorize : ∀ n → 0 < n  → PrimeFactors n
+factorize 0 0<0 = ⊥.rec (¬n<n 0<0)
+factorize 1 _ = pfs [] refl []
+factorize n@(suc (suc n-2)) _ = PF-aux n (primeOrComp n (n-2 , +-comm n-2 2))
diff --git a/Cubical/Data/Nat/Primes/Imports.agda b/Cubical/Data/Nat/Primes/Imports.agda
new file mode 100644
index 0000000000..9c8a078843
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Imports.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Imports where
+
+open import Cubical.Foundations.Prelude public
+open import Cubical.Foundations.Function public
+open import Cubical.Foundations.Isomorphism public
+
+open import Cubical.Data.Nat hiding (elim) public
+open import Cubical.Data.Nat.Order public
+open import Cubical.Data.Nat.Divisibility public
+open import Cubical.Data.Empty as ⊥ hiding (elim) public
+open import Cubical.Data.Unit public
+open import Cubical.Data.Sigma public
+open import Cubical.Data.List hiding (elim ; rec ; map) public
+open import Cubical.Data.Sum hiding (elim ; rec ; map) public
+open import Cubical.Relation.Nullary public
+open import Cubical.HITs.PropositionalTruncation hiding (map2 ; rec) public
+open import Cubical.Induction.WellFounded public
+open import Cubical.Data.Fin hiding (elim) public
diff --git a/Cubical/Data/Nat/Primes/Infinitude.agda b/Cubical/Data/Nat/Primes/Infinitude.agda
new file mode 100644
index 0000000000..e7d6b402a4
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Infinitude.agda
@@ -0,0 +1,61 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Infinitude where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Nat.Primes.Base
+open import Cubical.Data.Nat.Primes.Concrete
+open import Cubical.Data.Nat.Primes.Factors
+open import Cubical.Data.Nat.Primes.DecProps
+open import Cubical.Data.Nat.Count
+
+
+nextPrime : (n : ℕ) → Σ[ p ∈ ℕ ] ((n < p) × (isPrime p)) × ((z : ℕ) → (n < z) × isPrime z → p ≤ z)
+nextPrime n = findLeast (((newPrime n) .snd)) (DecProd (<Dec n) DecPrime)
+
+nthPrime : (n : ℕ) → Σ[ p ∈ ℕ ] isPrime p × (countBelow isPrime DecPrime p ≡ n)
+nthPrime zero = (least-prime .fst , least-prime .snd .fst , refl) where
+    least-prime = findLeast prime2 DecPrime
+nthPrime (suc n) = (next-prime .fst , next-prime .snd .fst .snd , snprimes) where
+    IH = nthPrime n
+
+    p#n = IH .fst
+    p#n-prime = IH .snd .fst
+    #p<p#n=n = IH .snd .snd
+
+    next-prime : Σ[ q ∈ ℕ ] ((p#n < q) × isPrime q) × (∀ z → (p#n < z) × isPrime z → q ≤ z)
+    next-prime = nextPrime p#n
+
+    q = next-prime .fst
+    p#n<q = next-prime .snd .fst .fst
+    p#n≤q = <-weaken p#n<q
+    q-prime = next-prime .snd .fst .snd
+    q-least = next-prime .snd .snd
+
+    sum : countBelow isPrime DecPrime q
+          ≡ countRange isPrime DecPrime p#n q p#n≤q + countBelow isPrime DecPrime p#n
+    sum = sym (countWorks isPrime DecPrime p#n q p#n≤q)
+    p1 : countRange isPrime DecPrime p#n q p#n≤q ≡ 1
+    p1 = leastAboveLow isPrime DecPrime p#n q p#n-prime
+         (isPropDec (primeProp p#n) (DecPrime p#n) (yes p#n-prime))
+         q-least p#n<q
+
+    snprimes : countBelow isPrime DecPrime q ≡ suc n
+    snprimes = sum ∙ add-equations p1 #p<p#n=n
+
+
+open Iso
+ℕ≅primeℕ : Iso ℕ (Σ ℕ isPrime)
+ℕ≅primeℕ .fun n = (pn .fst , pn .snd .fst) where pn = nthPrime n
+ℕ≅primeℕ .inv (p , _) = countBelow isPrime DecPrime p
+ℕ≅primeℕ .leftInv n = nthPrime n .snd .snd
+ℕ≅primeℕ .rightInv (p , p-prime) =
+    ΣPathP (answer , isProp→PathP (λ i → primeProp (answer i)) pn-prime p-prime) where
+        pn = nthPrime (countBelow isPrime DecPrime p)
+        pn-prime = pn .snd .fst
+        answer : pn .fst ≡ p
+        answer = countBelowYesInj isPrime DecPrime (pn .fst) p pn-prime p-prime
+                 (isPropDec (primeProp (pn .fst)) (DecPrime (pn .fst)) (yes pn-prime))
+                 (isPropDec (primeProp p) (DecPrime p) (yes p-prime))
+                 (pn .snd .snd)
diff --git a/Cubical/Data/Nat/Primes/Lemmas.agda b/Cubical/Data/Nat/Primes/Lemmas.agda
new file mode 100644
index 0000000000..8ac8ce0a07
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Lemmas.agda
@@ -0,0 +1,258 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Lemmas where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+private
+    variable
+        ℓ ℓ' ℓ'' : Level
+
+-- some successive implication syntax
+
+step⇒ : {A : Type ℓ} (B : Type ℓ') → (A → B) → A → B
+step⇒ _ f = f
+
+step⇒⟨⟩ : (A : Type ℓ) → A → A
+step⇒⟨⟩ A a = a
+
+syntax step⇒ B f x = x ⇒⟨ f ⟩ B
+syntax step⇒⟨⟩ A a = a ⇒⟨⟩ A
+infixl -9 step⇒ step⇒⟨⟩
+
+-- auxiliary inequality, multiplication, divisibility lemmas
+
+¬s<1 : ∀ {n} → ¬ suc n < 1
+¬s<1 sn<1 with (<-split sn<1)
+...     | inl sn<0 = ¬-<-zero sn<0
+...     | inr sn=0 = snotz sn=0
+
+¬z∣sn : ∀ n → ¬ 0 ∣ suc n
+¬z∣sn n z∣sn = ⊥.rec (znots (∣-zeroˡ z∣sn))
+
+¬<1∣sn : ∀ d n → d < 1 → ¬ d ∣ suc n
+¬<1∣sn d n d<1 d∣sn with (<-split d<1)
+...     | inr d=0 = ¬z∣sn n (subst (λ x → x ∣ suc n) d=0 (d∣sn))
+...     | inl d<0 = ¬-<-zero d<0
+
+1<→¬=0 : ∀ a → 1 < a → ¬ a ≡ 0
+1<→¬=0 a (b , b+2=a) a=0 = snotz (+-comm 2 b ∙ b+2=a ∙ a=0)
+
+<≠ : forall {m} {n} → m < n → ¬ m ≡ n
+<≠ {m = m} m<n m=n = <-asym m<n (0 , sym m=n)
+
+¬n<n : ∀ {n} → ¬ n < n
+¬n<n n<n = <≠ n<n refl
+
+z<suc : ∀ n → 0 < suc n
+z<suc n = n , +-suc n 0 ∙ cong suc (+-zero n)
+
+<1→0 : ∀ n → n < 1 → n ≡ 0
+<1→0 n n<1 with (<-split n<1)
+... | inr n=0 = n=0
+... | inl n<0 = ⊥.rec (¬-<-zero n<0)
+
+<<-asym : ∀ {a b} → a < b → ¬ b < a
+<<-asym {a} {b} a<b b<a = ¬n<n (<-trans a<b b<a)
+
+suc<-elim : ∀ {a} {b} → suc a < suc b → a < b
+suc<-elim {a} {b} (n , n+sa=b) = n , injSuc (subst (λ x → x ≡ suc b) (+-suc n (suc a)) n+sa=b)
+
+suc< : ∀ {a} {b} → a < b → suc a < suc b
+suc< {a} {b} (n , n+sa=b) = n , subst (λ x → x ≡ suc b) (sym (+-suc n (suc a))) (cong suc n+sa=b)
+
+add< : ∀ {a} {b} d → a < b → d + a < d + b
+add< zero a<b = a<b
+add< (suc d) a<b = suc< (add< d a<b)
+
+mult< : ∀ k a b → a < b → a · suc k < b · suc k
+mult< k a zero a<b = ⊥.rec (¬-<-zero a<b)
+mult< k zero (suc b) a<b = z<suc (k + b · suc k)
+mult< k (suc a) (suc b) a<b = suc< (add< k (mult< k a b (suc<-elim a<b)))
+
+lem1 : ∀ c k d n → c < k → k · (suc d) < n → c · (suc d) < n
+lem1 c k d n c<k ksd<n = <-trans (mult< d c k c<k) ksd<n
+
+lem2 : ∀ c k d n → k < c → n < d + k · d → n < d + c · d
+lem2 c k 0 n k<c n<k0 = ⊥.rec (¬-<-zero (subst (λ x → n < x) (sym (0≡m·0 k)) n<k0))
+lem2 c k d@(suc d-1) n k<c n<d+kd = <-trans n<d+kd (add< d (mult< d-1 k c k<c))
+
+sa<n : ∀ a n → suc a < n → a < n
+sa<n a n (k , k+ssa=n) = k + 1 , subst (λ x → x ≡ n) (+-assoc k 1 (suc a)) k+ssa=n
+
++a<n : ∀ k a n → k + a < n → a < n
++a<n zero a n a<n = a<n
++a<n (suc k) a n sk+a<n = +a<n k a n (sa<n (k + a) n sk+a<n)
+
+add-equations : ∀ {a} {b} {c} {d} → a ≡ b → c ≡ d → a + c ≡ b + d
+add-equations {b = b} {c = c} a=b c=d = cong (_+ c) a=b ∙ cong (b +_) c=d
+
+a·pos<n : ∀ a b n → a · suc b < n → a < n
+a·pos<n zero b n z<sucn = z<sucn
+a·pos<n (suc a) b zero asb<n = ⊥.rec (¬-<-zero asb<n)
+a·pos<n (suc a) b (suc n) asb<n = suc< (a·pos<n a b n (+a<n b (a · suc b) n (suc<-elim asb<n)))
+
+inj-·0< : ∀ {k} a b → 0 < k → k · a ≡ k · b → a ≡ b
+inj-·0< {zero} _ _ 0<0 _ = ⊥.rec (¬n<n 0<0)
+inj-·0< {suc k-1} a b 0<k = inj-sm· {m = k-1}
+
+n≤n·pos : ∀ n k → 0 < k → n ≤ n · k
+n≤n·pos n zero 0<0 = ⊥.rec (¬n<n 0<0)
+n≤n·pos n (suc k) _ = subst (λ x → n ≤ x) (sym (·-comm n (suc k))) ≤SumLeft
+
+1<·1<=3< : ∀ {a b} → 1 < a → 1 < b → 3 < a · b
+1<·1<=3< {0} {0} 1<a 1<b = ⊥.rec (1<→¬=0 0 1<a refl)
+1<·1<=3< {0} {suc b} 1<a 1<b = ⊥.rec (1<→¬=0 0 1<a refl)
+1<·1<=3< {suc a} {0} 1<a 1<b = ⊥.rec (1<→¬=0 0 1<b refl)
+1<·1<=3< {1} {suc b} 1<a 1<b = ⊥.rec (¬n<n 1<a)
+1<·1<=3< {suc (suc a)} {1} 1<a 1<b = ⊥.rec (¬n<n 1<b)
+1<·1<=3< {suc (suc a)} {suc (suc b)} 1<a 1<b =
+    suc< (suc< (<≤-trans (suc< (z<suc (b + a · suc (suc b)))) (≤SumRight {k = b})))
+
+PropFac< : ∀ a b n → 1 < b → 0 < n → a · b ≡ n → a < n
+PropFac< zero _ _ _ 0<n _ = 0<n
+PropFac< (suc a) zero n 1<b 0<n ab=n = ⊥.rec (¬-<-zero 1<b)
+PropFac< (suc a) (suc zero) n 1<b 0<n ab=n = ⊥.rec (¬n<n 1<b)
+PropFac< (suc a) (suc (suc b)) zero _ 0<n ab=n = ⊥.rec (¬n<n 0<n)
+PropFac< (suc a) (suc (suc b)) (suc n) _ _ ab=n = lem a b n ab=n where
+    lem : ∀ a b n → suc (suc (b + a · suc (suc b))) ≡ suc n → suc a < suc n
+    lem a b n p =
+        p :>                   suc (suc (b + a · suc (suc b))) ≡ suc n
+        ⇒⟨ injSuc ⟩                  suc (b + a · suc (suc b)) ≡ n
+        ⇒⟨ 0 ,_ ⟩                          b + a · suc (suc b) < n
+        ⇒⟨ +a<n b (a · suc (suc b)) n ⟩        a · suc (suc b) < n
+        ⇒⟨ a·pos<n a (suc b) n ⟩                             a < n
+        ⇒⟨ suc< ⟩                                        suc a < suc n
+
+∣+-cancel : ∀ n a b → n ∣ b → n ∣ (a + b) → n ∣ a
+∣+-cancel n a b tn∣b tn∣a+b = n∣a where
+    n∣b = ∣-untrunc tn∣b
+    n∣a+b = ∣-untrunc tn∣a+b
+
+    p = n∣b .fst
+    pn=b = n∣b .snd
+
+    q = n∣a+b .fst
+    qn=a+b = n∣a+b .snd
+
+    n∣a : n ∣ a
+    n∣a = ∣ (q ∸ p) , (
+            qn=a+b :>                                                    q · n ≡ a + b
+            ⇒⟨ subst (λ x → q · n ≡ a + x) (sym pn=b) ⟩                  q · n ≡ a + p · n
+            ⇒⟨ (λ x → cong (_∸ (p · n)) x ∙ +∸ a (p · n)) ⟩     q · n ∸ p · n ≡ a
+            ⇒⟨ (∸-distribʳ q p n) ∙_ ⟩                            (q ∸ p) · n ≡ a )
+         ∣₁
+
+
+ab=1→1 : ∀ a b → a · b ≡ 1 → b ≡ 1
+ab=1→1 0 0 ab=1 = ab=1
+ab=1→1 0 (suc b) ab=1 = ⊥.rec (znots ab=1)
+ab=1→1 (suc a) 0 ab=1 = ·-comm 0 a ∙ ab=1
+ab=1→1 (suc a) 1 _ = refl
+ab=1→1 (suc a) (suc (suc b)) ab=1 = ⊥.rec (snotz (injSuc ab=1))
+
+div1→1 : ∀ n → n ∣ 1 → n ≡ 1
+div1→1 n ∣n∣1∣ = ab=1→1 k n kn=1 where
+    n∣1 : Σ[ k ∈ ℕ ] k · n ≡ 1
+    n∣1 = ∣-untrunc ∣n∣1∣
+    k = n∣1 .fst
+    kn=1 = n∣1 .snd
+
+-- decidability lemmas
+
+Dec-1<k : ∀ k → Dec (1 < k)
+Dec-1<k k with (1 ≟ k)
+...     | lt 1<k = yes 1<k
+...     | eq 1=k = no (λ x → <≠ x 1=k)
+...     | gt k<1 = no (<<-asym k<1)
+
+Dec-k∣n :  ∀ {n} k → Dec (k ∣ n)
+Dec-k∣n {0} k = yes (∣-zeroʳ k)
+Dec-k∣n {n@(suc n-1)} k with (any? {n = n} (λ (x , _) → discreteℕ (x · k) n))
+...     | yes ((x , x<n) , xk=n) = yes (∣ (x , xk=n) ∣₁)
+...     | no bad with k
+...     | 0 = no (λ |ddiv| → ¬-<-zero (subst
+                                      (λ x → 0 < x)
+                                      (sym (subst
+                                           (λ x → 0 ≡ n)
+                                           (sym (0≡m·0 (fst (∣-untrunc |ddiv|))))
+                                           (snd (∣-untrunc |ddiv|))))
+                                       (z<suc n-1)))
+...     | 1 = yes (∣ n , ·-identityʳ n ∣₁)
+...     | suc (suc k) = no (λ |ddiv| → bad
+            ((fst (∣-untrunc |ddiv|) ,
+            PropFac< (fst (∣-untrunc |ddiv|)) (suc (suc k)) n
+                     (suc< (z<suc k)) (z<suc n-1) (snd (∣-untrunc |ddiv|))) ,
+            snd (∣-untrunc |ddiv|)))
+
+HasFactor : (n k : ℕ) → Type
+HasFactor n k = (1 < k) × (k ∣ n)
+
+DecHF : ∀ {n} k → Dec (HasFactor n k)
+DecHF k with (Dec-1<k k) | (Dec-k∣n k)
+... | (yes 1<k) | (yes k∣n) = yes (1<k , k∣n)
+... | (yes 1<k) | (no ¬k∣n) = no (λ (_ , k∣n) → ¬k∣n k∣n)
+... | (no ¬1<k) | _        = no (λ (1<k , _) → ¬1<k 1<k)
+
+-- find least natural with a given property, assuming there is one
+-- essentially the well-ordering principle: any inhabited subset has a least element
+
+findLeast-worker :
+        {n : ℕ} →
+        ({x : ℕ} → (x < n) → {P : ℕ → Type ℓ} → P x → (∀ a → Dec (P a)) →
+        Σ[ least ∈ ℕ ] (P least) × (∀ z → P z → least ≤ z)) →
+        {P : ℕ → Type ℓ} → P n → (∀ a → Dec (P a)) →
+        Σ[ least ∈ ℕ ] (P least) × (∀ z → P z → least ≤ z)
+findLeast-worker {n = zero} rec P0 Pdec = zero , (P0 , (λ _ _ → zero-≤))
+findLeast-worker {n = n@(suc n-1)} rec {P = P} Pn Pdec with any? {n = n} Qdec where
+    Qdec : ∀ ((x , x<n) : Fin n) → Dec (P x)
+    Qdec (x , x<n) = Pdec x
+... | yes ((x , x<n) , Px) = rec x<n Px Pdec
+... | no ¬x,x<n,Px = n , Pn , least where
+        least : ∀ x → P x → n ≤ x
+        least x Px with (Dichotomyℕ n x)
+        ... | inl n≤x = n≤x
+        ... | inr x<n = ⊥.rec (¬x,x<n,Px ((x , x<n) , Px))
+
+findLeast-explicit : (n : ℕ) → (P : ℕ → Type ℓ) → P n → (∀ a → Dec (P a)) →
+                     Σ[ least ∈ ℕ ] (P least) × (∀ z → P z → least ≤ z)
+findLeast-explicit = WFI.induction <-wellfounded
+                     (λ n rec P → findLeast-worker {n = n} (λ {x} x<n {P} → rec x x<n P) {P})
+
+findLeast : {n : ℕ} → {P : ℕ → Type ℓ} → P n → (∀ a → Dec (P a)) →
+            Σ[ least ∈ ℕ ] (P least) × (∀ z → P z → least ≤ z)
+findLeast {n = n} {P = P} = findLeast-explicit n P
+
+-- product and factorial lemmas for newPrime
+
+product : List ℕ → ℕ
+product [] = 1
+product (x ∷ xs) = x · product xs
+
+0<factorial : ∀ n → 0 < n !
+0<factorial 0 = z<suc 0
+0<factorial (suc n) = <≤-trans (0<factorial n) ≤SumLeft
+
+n≤! : ∀ n → n ≤ (n !)
+n≤! 0 = 1 , refl
+n≤! (suc n) = n≤n·pos (suc n) (n !) (0<factorial n)
+
+0<n∣n! : ∀ n → ¬ n ≡ 0 → n ∣ (n !)
+0<n∣n! zero ¬n=0 = ⊥.rec (¬n=0 refl)
+0<n∣n! (suc n) ¬n=0 = ∣ (n ! , ·-comm (n !) (suc n)) ∣₁
+
+≤n∣n! : ∀ a n → a ≤ n → ¬ a ≡ 0 → a ∣ (n !)
+≤n∣n! a zero a≤n ¬a=0 = ⊥.rec (¬a=0 (≤0→≡0 a≤n))
+≤n∣n! a (suc n) a≤sn na=0 with ≤-split a≤sn
+... | inr a=sn = subst (λ x → x ∣ ((suc n) !)) (sym a=sn) (0<n∣n! (suc n) snotz)
+... | inl (k , k+sa=sn) = ∣-trans a∣n! ∣ ((suc n) , refl) ∣₁ where
+    a∣n! : a ∣ (n !)
+    a∣n! = ≤n∣n! a n (k , injSuc (sym (+-suc k a) ∙ k+sa=sn)) na=0
+
+-- All
+
+data All {A : Type ℓ} (P : A → Type ℓ') : List A → Type (ℓ-max ℓ ℓ') where
+  []  :                             All P []
+  _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs)