From 779720e34503ab203f1019849e1089dfec9cb977 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 00:50:59 -0400
Subject: [PATCH 1/7] added Cubical.Data.Nat.Primes

---
 Cubical/Data/Nat/Primes/Base.agda       |  25 ++
 Cubical/Data/Nat/Primes/Concrete.agda   |  52 ++++
 Cubical/Data/Nat/Primes/DecProps.agda   | 104 ++++++++
 Cubical/Data/Nat/Primes/Factors.agda    | 109 ++++++++
 Cubical/Data/Nat/Primes/Imports.agda    |  20 ++
 Cubical/Data/Nat/Primes/Infinitude.agda |  61 +++++
 Cubical/Data/Nat/Primes/Lemmas.agda     | 321 ++++++++++++++++++++++++
 Cubical/Data/Nat/Primes/Split.agda      | 245 ++++++++++++++++++
 8 files changed, 937 insertions(+)
 create mode 100644 Cubical/Data/Nat/Primes/Base.agda
 create mode 100644 Cubical/Data/Nat/Primes/Concrete.agda
 create mode 100644 Cubical/Data/Nat/Primes/DecProps.agda
 create mode 100644 Cubical/Data/Nat/Primes/Factors.agda
 create mode 100644 Cubical/Data/Nat/Primes/Imports.agda
 create mode 100644 Cubical/Data/Nat/Primes/Infinitude.agda
 create mode 100644 Cubical/Data/Nat/Primes/Lemmas.agda
 create mode 100644 Cubical/Data/Nat/Primes/Split.agda

diff --git a/Cubical/Data/Nat/Primes/Base.agda b/Cubical/Data/Nat/Primes/Base.agda
new file mode 100644
index 0000000000..078feb4f0b
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Base.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe #-}
+
+module Cubical.Data.Nat.Primes.Base where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas using (1<·1<=3<)
+
+
+record isPrime (n : ℕ) : Type where
+    constructor prime
+    field
+        n-proper : 1 < n
+        primality : ∀ d → d ∣ n → (d ≡ 1) ⊎ (d ≡ n)
+
+record isComposite (n : ℕ) : Type where
+    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..8277198d9c
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/DecProps.agda
@@ -0,0 +1,104 @@
+{-# 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 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 (prime 1<n primality) (prime 1<n' primality') =
+    cong₂ prime
+    (isProp≤ 1<n 1<n')
+    (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) 1<n)
+    ))
+    primality primality' )
+
+compProp : ∀ n → isProp (isComposite n)
+compProp n (composite p q pp 1<q pq=n least) (composite p' q' pp' 1<q' pq=n' least') =
+    λ i → composite
+    (p=p' i)
+    (q=q' i)
+    ((isProp→PathP (λ j → primeProp (p=p' j)) pp pp') i)
+    ((isProp→PathP (λ j → isProp≤ {n = q=q' j}) 1<q 1<q') i)
+    ((isProp→PathP (λ j → isSetℕ (p=p' j · q=q' j) n) pq=n pq=n') i)
+    ((isProp→PathP (λ j → leastProp (p=p' j)) least least') i)
+    where
+        1<p : 1 < p
+        1<p = n-proper pp
+        1<p' : 1 < p'
+        1<p' = n-proper pp'
+
+        p∣n : p ∣ n
+        p∣n = ∣ (q , ·-comm q p ∙ pq=n) ∣₁
+        p'∣n : p' ∣ n
+        p'∣n = ∣ (q' , ·-comm q' p' ∙ pq=n') ∣₁
+
+        p=p' : p ≡ p'
+        p=p' = ≤-antisym (least p' 1<p' p'∣n) (least' p 1<p p∣n)
+
+        q=q' : q ≡ q'
+        q=q' = inj-·0< q q' (<-weaken 1<p) (pq=n ∙ sym (subst (λ x → x · q' ≡ n) (sym p=p') pq=n'))
+
+        leastProp : ∀ x → isProp ((p'' : ℕ) → 1 < p'' → p'' ∣ n → x ≤ p'')
+        leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
+
+prime→¬comp : ∀ n → isPrime n → ¬ isComposite n
+prime→¬comp n (prime 1<n primality) (composite p q pp 1<q pq=n _)
+    with (primality q ∣ (p , pq=n) ∣₁)
+... | inl q=1 = <≠ 1<q (sym q=1)
+... | inr q=n = <≠ (PropFac< q p n (n-proper pp) (<-weaken 1<n) (·-comm q p ∙ pq=n)) q=n
+
+¬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 λ (prime 1<0 _) → ¬-<-zero 1<0
+DecPrime 1 = no λ (prime 1<1 _) → ¬n<n 1<1
+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..d174f2be0e
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Factors.agda
@@ -0,0 +1,109 @@
+{-# 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))
+
+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 (composite p q pp 1<q pq=n least) with Dichotomyℕ p n
+... | inr n<p = p , n<p , pp
+... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 p p∣1))) where
+        1<p = pp .isPrime.n-proper
+        p∣1 : p ∣ 1
+        p∣1 = ∣+-cancel p 1 (n !) (≤n∣n! p n p≤n (1<→¬=0 p 1<p)) (∥_∥₁.∣ q , ·-comm q p ∙ pq=n ∣₁)
+
+
+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@(composite p q p-prime 1<q pq=n _) =
+    pfs (p ∷ primes qFacs)
+        (subst (λ x → p · x ≡ n) (sym (factored qFacs)) pq=n)
+        (p-prime ∷ allPrime qFacs)
+        where
+            qFacs : PrimeFactors q
+            qFacs with (primeOrComp q 1<q)
+            ... | inl qp = PF-prime q qp
+            ... | inr qc = rec q (PropFac< q p n 1<p 0<n (·-comm q p ∙ pq=n)) qc where
+                    1<p = isPrime.n-proper p-prime
+                    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..81de7253d4
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Infinitude.agda
@@ -0,0 +1,61 @@
+{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+
+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.Split
+open import Cubical.Data.Nat.Primes.Concrete
+open import Cubical.Data.Nat.Primes.Factors
+open import Cubical.Data.Nat.Primes.DecProps
+
+
+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)
+fun      ℕ≅primeℕ n = (pn .fst , pn .snd .fst) where pn = nthPrime n
+inv      ℕ≅primeℕ (p , _) = countBelow isPrime DecPrime p
+leftInv  ℕ≅primeℕ n = nthPrime n .snd .snd
+rightInv ℕ≅primeℕ (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..cdcdfb9e6a
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Lemmas.agda
@@ -0,0 +1,321 @@
+{-# 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 2 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)
+
+¬a+sn=n : ∀ {a} n → ¬ a + suc n ≡ n
+¬a+sn=n {a} zero a+sn=n = snotz (subst (λ x → x ≡ 0) (+-suc a 0) a+sn=n)
+¬a+sn=n {a} (suc n) a+sn=n = ¬a+sn=n n (injSuc (subst (λ x → x ≡ suc n) (+-suc a (suc n)) a+sn=n))
+
+<≠ : forall {m} {n} → m < n → ¬ m ≡ n
+<≠ {m = m} (a , a+sm=n) m=n = ¬a+sn=n m (subst (λ x → a + suc m ≡ x) (sym m=n) a+sm=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
+          →⟨ 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
+              →⟨ 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<n : ∀ k → Dec (1 < k)
+Dec-1<n 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|)))
+
+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)
+
+DecToSum : {A : Type ℓ} → (Dec A) → (A ⊎ (¬ A))
+DecToSum (yes a) = inl a
+DecToSum (no ¬a) = inr ¬a
+
+×-≡elim : {A : Type ℓ} {B : Type ℓ'} → {(a , b) (a' , b') : (A × B)} →
+          ((a , b) ≡ (a' , b')) → (a ≡ a') × (b ≡ b')
+×-≡elim p = (λ i → p i .fst) , (λ i → p i .snd)
+
+DecProd-aux-inj : {A : Type ℓ} (P : A → Type ℓ') (Q : A → Type ℓ'') → ∀ {a} →
+                  (DPa : Dec (P a)) → (DQa : Dec (Q a)) → (Pa : P a) → (Qa : Q a) →
+                  (DecProd-aux P Q DPa DQa ≡ DecProd-aux P Q (yes Pa) (yes Qa)) →
+                  (DPa ≡ yes Pa) × (DQa ≡ yes Qa)
+DecProd-aux-inj P Q (yes p₁) (no ¬p) Pa Qa p = ⊥.rec (¬p Qa)
+DecProd-aux-inj P Q (no ¬p) (yes p₁) Pa Qa p = ⊥.rec (¬p Pa)
+DecProd-aux-inj P Q (no ¬p) (no ¬p₁) Pa Qa p = ⊥.rec (¬p Pa)
+DecProd-aux-inj P Q (yes Pa') (yes Qa') Pa Qa y'=y = cong yes (pq .fst) , cong yes (pq .snd) where
+    inlPQ'=inlPQ : inl (Pa' , Qa') ≡ inl (Pa , Qa)
+    inlPQ'=inlPQ = cong DecToSum y'=y
+    Pa'Qa'=PaQa : (Pa' , Qa') ≡ (Pa , Qa)
+    Pa'Qa'=PaQa = lower (⊎Path.encode (inl (Pa' , Qa')) (inl (Pa , Qa)) inlPQ'=inlPQ)
+    pq : (Pa' ≡ Pa) × (Qa' ≡ Qa)
+    pq = ×-≡elim Pa'Qa'=PaQa
+
+DecProdComp : {A : Type ℓ} {P : A → Type ℓ'} {Q : A → Type ℓ''} →
+              (Pdec : ∀ a → Dec (P a)) → (Qdec : ∀ a → Dec (Q a)) → (a : A) →
+              (Pa : P a) → (Qa : Q a) → (DecProd Pdec Qdec) a ≡ yes (Pa , Qa) →
+              (Pdec a ≡ yes Pa) × (Qdec a ≡ yes Qa)
+DecProdComp {P = P} {Q = Q} Pdec Qdec a = DecProd-aux-inj P Q (Pdec a) (Qdec a)
+
+HasFactor : (n k : ℕ) → Type
+HasFactor n k = (1 < k) × (k ∣ n)
+
+DecHF : ∀ {n} k → Dec (HasFactor n k)
+DecHF = DecProd Dec-1<n Dec-k∣n
+
+-- a few helpers for using DecProdComp with a contractible type
+
+×contrIso : (A : Type ℓ) (B : Type ℓ') → isContr B → Iso (A × B) A
+×contrIso A B (b0 , contract) = iso fst (_, b0) (λ b → refl) (λ (a , b) → ≡-× refl (contract b))
+
+≤-0contr : {n : ℕ} → isContr (0 ≤ n)
+≤-0contr = zero-≤ , (isProp≤ zero-≤)
+
+P×0≤=P : (P : ℕ → Type ℓ) (n : ℕ) → ((P n) × (0 ≤ n)) ≡ P n
+P×0≤=P P n = isoToPath (×contrIso (P n) (0 ≤ n) ≤-0contr)
+
+-- 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 and mapAll
+
+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
diff --git a/Cubical/Data/Nat/Primes/Split.agda b/Cubical/Data/Nat/Primes/Split.agda
new file mode 100644
index 0000000000..656a4c7f7f
--- /dev/null
+++ b/Cubical/Data/Nat/Primes/Split.agda
@@ -0,0 +1,245 @@
+{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+
+module Cubical.Data.Nat.Primes.Split where
+
+open import Cubical.Data.Nat.Primes.Imports
+open import Cubical.Data.Nat.Primes.Lemmas
+open import Cubical.Data.Empty as ⊥ hiding (elim)
+
+
+private
+    variable
+        ℓ ℓ' : Level
+
+    decToN : {A : Type ℓ} → Dec A → ℕ
+    decToN (yes _) = 1
+    decToN (no  _) = 0
+
+-- 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))
+
+
+
+    -- cRange0≡cBelow : (n : ℕ) → countRange 0 n zero-≤ ≡ countBelow n
+    -- cRange0≡cBelow n = cong length
+    --              (cong₂ (λ Q Qdec → splitBelow Q Qdec n .fst .fst)
+    --                     (funExt (P×0≤=P P))
+    --                     (funExt lem)) where
+    --     lem : (x : ℕ) → PathP (λ i → Dec (funExt (P×0≤=P P) i x))
+    --                           (DecProd Pdec (≤Dec 0) x) (Pdec x)
+    --     lem x = toPathP answer where
+    --         answer-aux : (compProd : Dec (funExt (P×0≤=P P) i0 x)) →
+    --                      (DecProd Pdec (≤Dec 0) x) ≡ compProd →
+    --                      (compPdec : Dec (P x)) → Pdec x ≡ compPdec →
+    --                      transport (λ i → Dec (funExt (P×0≤=P P) i x)) compProd ≡ Pdec x
+    --         answer-aux (yes (Px , 0≤x)) p _ _ =
+    --             sym (DecProdComp
+    --                     Pdec (≤Dec 0) x Px zero-≤
+    --                     (p ∙ cong (λ ineq → yes (Px , ineq)) (isProp≤ _ _)) .fst
+    --                     ∙ cong yes (λ i → transp (λ j → P x) (~ i) Px))
+    --         answer-aux (no ¬Px0≤x) _ (yes Px) p2 = ⊥.rec (¬Px0≤x (Px , zero-≤))
+    --         answer-aux (no _) _ (no _) p2 = cong no (isProp¬ (P x) _ _) ∙ sym p2
+    --         answer : transport (λ i → Dec (funExt (P×0≤=P P) i x)) (DecProd Pdec (≤Dec 0) x)
+    --                  ≡ Pdec x
+    --         answer = answer-aux (DecProd Pdec (≤Dec 0) x) refl (Pdec x) refl

From 4b990905127c421194e481f1e89bd8903e2f9b71 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 00:56:27 -0400
Subject: [PATCH 2/7] removed commented-out code

---
 Cubical/Data/Nat/Primes/Split.agda | 25 -------------------------
 1 file changed, 25 deletions(-)

diff --git a/Cubical/Data/Nat/Primes/Split.agda b/Cubical/Data/Nat/Primes/Split.agda
index 656a4c7f7f..91adb5722b 100644
--- a/Cubical/Data/Nat/Primes/Split.agda
+++ b/Cubical/Data/Nat/Primes/Split.agda
@@ -218,28 +218,3 @@ module _ (P : ℕ → Type ℓ) (Pdec : ∀ n → Dec (P n)) where
     ... | 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))
-
-
-
-    -- cRange0≡cBelow : (n : ℕ) → countRange 0 n zero-≤ ≡ countBelow n
-    -- cRange0≡cBelow n = cong length
-    --              (cong₂ (λ Q Qdec → splitBelow Q Qdec n .fst .fst)
-    --                     (funExt (P×0≤=P P))
-    --                     (funExt lem)) where
-    --     lem : (x : ℕ) → PathP (λ i → Dec (funExt (P×0≤=P P) i x))
-    --                           (DecProd Pdec (≤Dec 0) x) (Pdec x)
-    --     lem x = toPathP answer where
-    --         answer-aux : (compProd : Dec (funExt (P×0≤=P P) i0 x)) →
-    --                      (DecProd Pdec (≤Dec 0) x) ≡ compProd →
-    --                      (compPdec : Dec (P x)) → Pdec x ≡ compPdec →
-    --                      transport (λ i → Dec (funExt (P×0≤=P P) i x)) compProd ≡ Pdec x
-    --         answer-aux (yes (Px , 0≤x)) p _ _ =
-    --             sym (DecProdComp
-    --                     Pdec (≤Dec 0) x Px zero-≤
-    --                     (p ∙ cong (λ ineq → yes (Px , ineq)) (isProp≤ _ _)) .fst
-    --                     ∙ cong yes (λ i → transp (λ j → P x) (~ i) Px))
-    --         answer-aux (no ¬Px0≤x) _ (yes Px) p2 = ⊥.rec (¬Px0≤x (Px , zero-≤))
-    --         answer-aux (no _) _ (no _) p2 = cong no (isProp¬ (P x) _ _) ∙ sym p2
-    --         answer : transport (λ i → Dec (funExt (P×0≤=P P) i x)) (DecProd Pdec (≤Dec 0) x)
-    --                  ≡ Pdec x
-    --         answer = answer-aux (DecProd Pdec (≤Dec 0) x) refl (Pdec x) refl

From 4d5d4ba9c3ade4ff7b448006ddbb36ed58c99101 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 15:07:58 -0400
Subject: [PATCH 3/7] removed unused code, made changes according to
 suggestions

---
 Cubical/Data/Nat/Primes/Base.agda       |  8 ++-
 Cubical/Data/Nat/Primes/Infinitude.agda |  2 +-
 Cubical/Data/Nat/Primes/Lemmas.agda     | 82 +++++--------------------
 Cubical/Data/Nat/Primes/Split.agda      |  2 +-
 4 files changed, 26 insertions(+), 68 deletions(-)

diff --git a/Cubical/Data/Nat/Primes/Base.agda b/Cubical/Data/Nat/Primes/Base.agda
index 078feb4f0b..ef9af8b4d4 100644
--- a/Cubical/Data/Nat/Primes/Base.agda
+++ b/Cubical/Data/Nat/Primes/Base.agda
@@ -2,17 +2,23 @@
 
 module Cubical.Data.Nat.Primes.Base where
 
-open import Cubical.Data.Nat.Primes.Imports
+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 : ℕ
diff --git a/Cubical/Data/Nat/Primes/Infinitude.agda b/Cubical/Data/Nat/Primes/Infinitude.agda
index 81de7253d4..fec81c543e 100644
--- a/Cubical/Data/Nat/Primes/Infinitude.agda
+++ b/Cubical/Data/Nat/Primes/Infinitude.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+{-# OPTIONS --safe #-}
 
 module Cubical.Data.Nat.Primes.Infinitude where
 
diff --git a/Cubical/Data/Nat/Primes/Lemmas.agda b/Cubical/Data/Nat/Primes/Lemmas.agda
index cdcdfb9e6a..0fa3b659d8 100644
--- a/Cubical/Data/Nat/Primes/Lemmas.agda
+++ b/Cubical/Data/Nat/Primes/Lemmas.agda
@@ -12,15 +12,15 @@ private
 
 -- some successive implication syntax
 
-step→ : {A : Type ℓ} (B : Type ℓ') → (A → B) → A → B
-step→ _ f = f
+step⇒ : {A : Type ℓ} (B : Type ℓ') → (A → B) → A → B
+step⇒ _ f = f
 
-step→⟨⟩ : (A : Type ℓ) → A → A
-step→⟨⟩ A a = a
+step⇒⟨⟩ : (A : Type ℓ) → A → A
+step⇒⟨⟩ A a = a
 
-syntax step→ B f x = x →⟨ f ⟩ B
-syntax step→⟨⟩ A a = a →⟨⟩ A
-infixl 2 step→ step→⟨⟩
+syntax step⇒ B f x = x ⇒⟨ f ⟩ B
+syntax step⇒⟨⟩ A a = a ⇒⟨⟩ A
+infixl -9 step⇒ step⇒⟨⟩
 
 -- auxiliary inequality, multiplication, divisibility lemmas
 
@@ -123,17 +123,12 @@ 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
-          →⟨ 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
+        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
@@ -148,13 +143,10 @@ PropFac< (suc a) (suc (suc b)) (suc n) _ _ ab=n = lem a b n ab=n where
 
     n∣a : n ∣ a
     n∣a = ∣ (q ∸ p) , (
-            qn=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 )
+            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 )
          ∣₁
 
 
@@ -209,52 +201,12 @@ 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)
 
-DecToSum : {A : Type ℓ} → (Dec A) → (A ⊎ (¬ A))
-DecToSum (yes a) = inl a
-DecToSum (no ¬a) = inr ¬a
-
-×-≡elim : {A : Type ℓ} {B : Type ℓ'} → {(a , b) (a' , b') : (A × B)} →
-          ((a , b) ≡ (a' , b')) → (a ≡ a') × (b ≡ b')
-×-≡elim p = (λ i → p i .fst) , (λ i → p i .snd)
-
-DecProd-aux-inj : {A : Type ℓ} (P : A → Type ℓ') (Q : A → Type ℓ'') → ∀ {a} →
-                  (DPa : Dec (P a)) → (DQa : Dec (Q a)) → (Pa : P a) → (Qa : Q a) →
-                  (DecProd-aux P Q DPa DQa ≡ DecProd-aux P Q (yes Pa) (yes Qa)) →
-                  (DPa ≡ yes Pa) × (DQa ≡ yes Qa)
-DecProd-aux-inj P Q (yes p₁) (no ¬p) Pa Qa p = ⊥.rec (¬p Qa)
-DecProd-aux-inj P Q (no ¬p) (yes p₁) Pa Qa p = ⊥.rec (¬p Pa)
-DecProd-aux-inj P Q (no ¬p) (no ¬p₁) Pa Qa p = ⊥.rec (¬p Pa)
-DecProd-aux-inj P Q (yes Pa') (yes Qa') Pa Qa y'=y = cong yes (pq .fst) , cong yes (pq .snd) where
-    inlPQ'=inlPQ : inl (Pa' , Qa') ≡ inl (Pa , Qa)
-    inlPQ'=inlPQ = cong DecToSum y'=y
-    Pa'Qa'=PaQa : (Pa' , Qa') ≡ (Pa , Qa)
-    Pa'Qa'=PaQa = lower (⊎Path.encode (inl (Pa' , Qa')) (inl (Pa , Qa)) inlPQ'=inlPQ)
-    pq : (Pa' ≡ Pa) × (Qa' ≡ Qa)
-    pq = ×-≡elim Pa'Qa'=PaQa
-
-DecProdComp : {A : Type ℓ} {P : A → Type ℓ'} {Q : A → Type ℓ''} →
-              (Pdec : ∀ a → Dec (P a)) → (Qdec : ∀ a → Dec (Q a)) → (a : A) →
-              (Pa : P a) → (Qa : Q a) → (DecProd Pdec Qdec) a ≡ yes (Pa , Qa) →
-              (Pdec a ≡ yes Pa) × (Qdec a ≡ yes Qa)
-DecProdComp {P = P} {Q = Q} Pdec Qdec a = DecProd-aux-inj P Q (Pdec a) (Qdec a)
-
 HasFactor : (n k : ℕ) → Type
 HasFactor n k = (1 < k) × (k ∣ n)
 
 DecHF : ∀ {n} k → Dec (HasFactor n k)
 DecHF = DecProd Dec-1<n Dec-k∣n
 
--- a few helpers for using DecProdComp with a contractible type
-
-×contrIso : (A : Type ℓ) (B : Type ℓ') → isContr B → Iso (A × B) A
-×contrIso A B (b0 , contract) = iso fst (_, b0) (λ b → refl) (λ (a , b) → ≡-× refl (contract b))
-
-≤-0contr : {n : ℕ} → isContr (0 ≤ n)
-≤-0contr = zero-≤ , (isProp≤ zero-≤)
-
-P×0≤=P : (P : ℕ → Type ℓ) (n : ℕ) → ((P n) × (0 ≤ n)) ≡ P n
-P×0≤=P P n = isoToPath (×contrIso (P n) (0 ≤ n) ≤-0contr)
-
 -- find least natural with a given property, assuming there is one
 -- essentially the well-ordering principle: any inhabited subset has a least element
 
diff --git a/Cubical/Data/Nat/Primes/Split.agda b/Cubical/Data/Nat/Primes/Split.agda
index 91adb5722b..acd08a484b 100644
--- a/Cubical/Data/Nat/Primes/Split.agda
+++ b/Cubical/Data/Nat/Primes/Split.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe -W noUnsupportedIndexedMatch #-}
+{-# OPTIONS --safe #-}
 
 module Cubical.Data.Nat.Primes.Split where
 

From 4fc04fe702693feadfc83df689a407c198dc3167 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 17:44:42 -0400
Subject: [PATCH 4/7] added no-eta-equality to isPrime and isComposite

---
 Cubical/Data/Nat/Primes/Base.agda     |   4 +-
 Cubical/Data/Nat/Primes/DecProps.agda | 178 ++++++++++++++++++++------
 Cubical/Data/Nat/Primes/Factors.agda  |  39 +++---
 3 files changed, 166 insertions(+), 55 deletions(-)

diff --git a/Cubical/Data/Nat/Primes/Base.agda b/Cubical/Data/Nat/Primes/Base.agda
index ef9af8b4d4..895e3324e9 100644
--- a/Cubical/Data/Nat/Primes/Base.agda
+++ b/Cubical/Data/Nat/Primes/Base.agda
@@ -11,14 +11,14 @@ open import Cubical.Data.Nat.Primes.Lemmas using (1<·1<=3<)
 
 
 record isPrime (n : ℕ) : Type where
-    -- no-eta-equality
+    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
+    no-eta-equality
     constructor composite
     field
         p q : ℕ
diff --git a/Cubical/Data/Nat/Primes/DecProps.agda b/Cubical/Data/Nat/Primes/DecProps.agda
index 8277198d9c..2ff4938b62 100644
--- a/Cubical/Data/Nat/Primes/DecProps.agda
+++ b/Cubical/Data/Nat/Primes/DecProps.agda
@@ -8,6 +8,7 @@ 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
@@ -23,50 +24,151 @@ private
     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 (prime 1<n primality) (prime 1<n' primality') =
-    cong₂ prime
-    (isProp≤ 1<n 1<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) 1<n)
-    ))
-    primality primality' )
+    λ 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 (composite p q pp 1<q pq=n least) (composite p' q' pp' 1<q' pq=n' least') =
-    λ i → composite
-    (p=p' i)
-    (q=q' i)
-    ((isProp→PathP (λ j → primeProp (p=p' j)) pp pp') i)
-    ((isProp→PathP (λ j → isProp≤ {n = q=q' j}) 1<q 1<q') i)
-    ((isProp→PathP (λ j → isSetℕ (p=p' j · q=q' j) n) pq=n pq=n') i)
-    ((isProp→PathP (λ j → leastProp (p=p' j)) least least') i)
-    where
-        1<p : 1 < p
-        1<p = n-proper pp
-        1<p' : 1 < p'
-        1<p' = n-proper pp'
-
-        p∣n : p ∣ n
-        p∣n = ∣ (q , ·-comm q p ∙ pq=n) ∣₁
-        p'∣n : p' ∣ n
-        p'∣n = ∣ (q' , ·-comm q' p' ∙ pq=n') ∣₁
-
-        p=p' : p ≡ p'
-        p=p' = ≤-antisym (least p' 1<p' p'∣n) (least' p 1<p p∣n)
-
-        q=q' : q ≡ q'
-        q=q' = inj-·0< q q' (<-weaken 1<p) (pq=n ∙ sym (subst (λ x → x · q' ≡ n) (sym p=p') pq=n'))
-
-        leastProp : ∀ x → isProp ((p'' : ℕ) → 1 < p'' → p'' ∣ n → x ≤ p'')
+compProp n nc nc' i .p = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n) i where
+        least1 = nc .least
+        least2 = nc' .least
+        p1 = nc .p
+        p2 = nc' .p
+        pp1 = nc .p-prime
+        pp2 = nc' .p-prime
+        1<p1 = pp1 .n-proper
+        1<p2 = pp2 .n-proper
+        q1 = nc .q
+        q2 = nc' .q
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        p1∣n = ∣ (q1 , ·-comm q1 p1 ∙ pq=n) ∣₁
+        p2∣n = ∣ (q2 , ·-comm q2 p2 ∙ pq=n') ∣₁
+
+compProp n nc nc' i .q = q1=q2 i 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
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        1<q1 = nc .q-proper
+        1<q2 = nc' .q-proper
+        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'))
+
+compProp n nc nc' i .p-prime = (isProp→PathP (λ j → primeProp (p1=p2 j)) pp1 pp2) i 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
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        1<q1 = nc .q-proper
+        1<q2 = nc' .q-proper
+        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)
+
+compProp n nc nc' i .q-proper = (isProp→PathP (λ j → isProp≤ {n = q1=q2 j}) 1<q1 1<q2) i 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
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        1<q1 = nc .q-proper
+        1<q2 = nc' .q-proper
+        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'))
+
+compProp n nc nc' i .factors = (isProp→PathP (λ j → isSetℕ (p1=p2 j · q1=q2 j) n) pq=n pq=n') i 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
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        1<q1 = nc .q-proper
+        1<q2 = nc' .q-proper
+        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'))
+
+compProp n nc nc' i .least = (isProp→PathP (λ j → leastProp (p1=p2 j)) least1 least2) i 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
+        pq=n = nc .factors
+        pq=n' = nc' .factors
+        1<q1 = nc .q-proper
+        1<q2 = nc' .q-proper
+        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)
+        leastProp : ∀ x → isProp ((p2' : ℕ) → 1 < p2' → p2' ∣ n → x ≤ p2')
         leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
 
+
+
 prime→¬comp : ∀ n → isPrime n → ¬ isComposite n
-prime→¬comp n (prime 1<n primality) (composite p q pp 1<q pq=n _)
-    with (primality q ∣ (p , pq=n) ∣₁)
-... | inl q=1 = <≠ 1<q (sym q=1)
-... | inr q=n = <≠ (PropFac< q p n (n-proper pp) (<-weaken 1<n) (·-comm q p ∙ pq=n)) q=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
@@ -90,8 +192,8 @@ 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 λ (prime 1<0 _) → ¬-<-zero 1<0
-DecPrime 1 = no λ (prime 1<1 _) → ¬n<n 1<1
+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)
diff --git a/Cubical/Data/Nat/Primes/Factors.agda b/Cubical/Data/Nat/Primes/Factors.agda
index d174f2be0e..ed66a64f6a 100644
--- a/Cubical/Data/Nat/Primes/Factors.agda
+++ b/Cubical/Data/Nat/Primes/Factors.agda
@@ -59,15 +59,18 @@ primeOrComp n@(suc n-1) 1<n = answer where
                                                         (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 (composite p q pp 1<q pq=n least) with Dichotomyℕ p n
-... | inr n<p = p , n<p , pp
-... | inl p≤n = ⊥.rec (<≠ 1<p (sym (div1→1 p p∣1))) where
-        1<p = pp .isPrime.n-proper
-        p∣1 : p ∣ 1
-        p∣1 = ∣+-cancel p 1 (n !) (≤n∣n! p n p≤n (1<→¬=0 p 1<p)) (∥_∥₁.∣ q , ·-comm q p ∙ pq=n ∣₁)
+... | 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
@@ -84,16 +87,22 @@ 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@(composite p q p-prime 1<q pq=n _) =
-    pfs (p ∷ primes qFacs)
-        (subst (λ x → p · x ≡ n) (sym (factored qFacs)) pq=n)
-        (p-prime ∷ allPrime qFacs)
+PF-comp-work n rec nComp =
+    pfs (pfac ∷ primes qFacs)
+        (subst (λ x → pfac · x ≡ n) (sym (factored qFacs)) pq=n)
+        (pp ∷ allPrime qFacs)
         where
-            qFacs : PrimeFactors q
-            qFacs with (primeOrComp q 1<q)
-            ... | inl qp = PF-prime q qp
-            ... | inr qc = rec q (PropFac< q p n 1<p 0<n (·-comm q p ∙ pq=n)) qc where
-                    1<p = isPrime.n-proper p-prime
+            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

From 8cd16b932726ce219aee0b2aa1ef60bf40c918aa Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 18:03:43 -0400
Subject: [PATCH 5/7] cleaned up awfulness

---
 Cubical/Data/Nat/Primes/DecProps.agda | 160 ++++++--------------------
 1 file changed, 35 insertions(+), 125 deletions(-)

diff --git a/Cubical/Data/Nat/Primes/DecProps.agda b/Cubical/Data/Nat/Primes/DecProps.agda
index 2ff4938b62..d957eb1ee9 100644
--- a/Cubical/Data/Nat/Primes/DecProps.agda
+++ b/Cubical/Data/Nat/Primes/DecProps.agda
@@ -33,132 +33,42 @@ primeProp n np np' i .primality =
     λ 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' i .p = ≤-antisym (least1 p2 1<p2 p2∣n) (least2 p1 1<p1 p1∣n) i where
-        least1 = nc .least
-        least2 = nc' .least
-        p1 = nc .p
-        p2 = nc' .p
-        pp1 = nc .p-prime
-        pp2 = nc' .p-prime
-        1<p1 = pp1 .n-proper
-        1<p2 = pp2 .n-proper
-        q1 = nc .q
-        q2 = nc' .q
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        p1∣n = ∣ (q1 , ·-comm q1 p1 ∙ pq=n) ∣₁
-        p2∣n = ∣ (q2 , ·-comm q2 p2 ∙ pq=n') ∣₁
-
-compProp n nc nc' i .q = q1=q2 i 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
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        1<q1 = nc .q-proper
-        1<q2 = nc' .q-proper
-        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'))
-
-compProp n nc nc' i .p-prime = (isProp→PathP (λ j → primeProp (p1=p2 j)) pp1 pp2) i 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
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        1<q1 = nc .q-proper
-        1<q2 = nc' .q-proper
-        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)
-
-compProp n nc nc' i .q-proper = (isProp→PathP (λ j → isProp≤ {n = q1=q2 j}) 1<q1 1<q2) i 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
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        1<q1 = nc .q-proper
-        1<q2 = nc' .q-proper
-        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'))
-
-compProp n nc nc' i .factors = (isProp→PathP (λ j → isSetℕ (p1=p2 j · q1=q2 j) n) pq=n pq=n') i 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
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        1<q1 = nc .q-proper
-        1<q2 = nc' .q-proper
-        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'))
-
-compProp n nc nc' i .least = (isProp→PathP (λ j → leastProp (p1=p2 j)) least1 least2) i 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
-        pq=n = nc .factors
-        pq=n' = nc' .factors
-        1<q1 = nc .q-proper
-        1<q2 = nc' .q-proper
-        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)
-        leastProp : ∀ x → isProp ((p2' : ℕ) → 1 < p2' → p2' ∣ n → x ≤ p2')
-        leastProp x = funcProp (λ a → funcProp (λ 1<a → funcProp (λ a∣n → isProp≤)))
-
+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

From 9642bf58002c5214f4d99ec2fe38260fae196f20 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 18:07:35 -0400
Subject: [PATCH 6/7] aesthetic change

---
 Cubical/Data/Nat/Primes/Infinitude.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cubical/Data/Nat/Primes/Infinitude.agda b/Cubical/Data/Nat/Primes/Infinitude.agda
index fec81c543e..9b44949737 100644
--- a/Cubical/Data/Nat/Primes/Infinitude.agda
+++ b/Cubical/Data/Nat/Primes/Infinitude.agda
@@ -47,10 +47,10 @@ nthPrime (suc n) = (next-prime .fst , next-prime .snd .fst .snd , snprimes) wher
 
 open Iso
 ℕ≅primeℕ : Iso ℕ (Σ ℕ isPrime)
-fun      ℕ≅primeℕ n = (pn .fst , pn .snd .fst) where pn = nthPrime n
-inv      ℕ≅primeℕ (p , _) = countBelow isPrime DecPrime p
-leftInv  ℕ≅primeℕ n = nthPrime n .snd .snd
-rightInv ℕ≅primeℕ (p , p-prime) =
+ℕ≅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

From 0fca3b57425543c3fda53f40497f35b3681144f6 Mon Sep 17 00:00:00 2001
From: Adam Kleber <adam.kleber@gmail.com>
Date: Wed, 16 Jul 2025 22:36:04 -0400
Subject: [PATCH 7/7] renamed Split to Count and moved it out of Primes

---
 .../Nat/{Primes/Split.agda => Count.agda}     | 43 +++++++++++++++++--
 Cubical/Data/Nat/Primes/Infinitude.agda       |  2 +-
 Cubical/Data/Nat/Primes/Lemmas.agda           | 31 ++++---------
 3 files changed, 48 insertions(+), 28 deletions(-)
 rename Cubical/Data/Nat/{Primes/Split.agda => Count.agda} (86%)

diff --git a/Cubical/Data/Nat/Primes/Split.agda b/Cubical/Data/Nat/Count.agda
similarity index 86%
rename from Cubical/Data/Nat/Primes/Split.agda
rename to Cubical/Data/Nat/Count.agda
index acd08a484b..45644c9a39 100644
--- a/Cubical/Data/Nat/Primes/Split.agda
+++ b/Cubical/Data/Nat/Count.agda
@@ -1,20 +1,55 @@
 {-# OPTIONS --safe #-}
 
-module Cubical.Data.Nat.Primes.Split where
+module Cubical.Data.Nat.Count where
 
-open import Cubical.Data.Nat.Primes.Imports
-open import Cubical.Data.Nat.Primes.Lemmas
+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
+        ℓ ℓ' ℓ'' : 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
diff --git a/Cubical/Data/Nat/Primes/Infinitude.agda b/Cubical/Data/Nat/Primes/Infinitude.agda
index 9b44949737..e7d6b402a4 100644
--- a/Cubical/Data/Nat/Primes/Infinitude.agda
+++ b/Cubical/Data/Nat/Primes/Infinitude.agda
@@ -5,10 +5,10 @@ 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.Split
 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)
diff --git a/Cubical/Data/Nat/Primes/Lemmas.agda b/Cubical/Data/Nat/Primes/Lemmas.agda
index 0fa3b659d8..8ac8ce0a07 100644
--- a/Cubical/Data/Nat/Primes/Lemmas.agda
+++ b/Cubical/Data/Nat/Primes/Lemmas.agda
@@ -40,12 +40,8 @@ infixl -9 step⇒ step⇒⟨⟩
 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)
 
-¬a+sn=n : ∀ {a} n → ¬ a + suc n ≡ n
-¬a+sn=n {a} zero a+sn=n = snotz (subst (λ x → x ≡ 0) (+-suc a 0) a+sn=n)
-¬a+sn=n {a} (suc n) a+sn=n = ¬a+sn=n n (injSuc (subst (λ x → x ≡ suc n) (+-suc a (suc n)) a+sn=n))
-
 <≠ : forall {m} {n} → m < n → ¬ m ≡ n
-<≠ {m = m} (a , a+sm=n) m=n = ¬a+sn=n m (subst (λ x → a + suc m ≡ x) (sym m=n) a+sm=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
@@ -166,8 +162,8 @@ div1→1 n ∣n∣1∣ = ab=1→1 k n kn=1 where
 
 -- decidability lemmas
 
-Dec-1<n : ∀ k → Dec (1 < k)
-Dec-1<n k with (1 ≟ k)
+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)
@@ -191,21 +187,14 @@ Dec-k∣n {n@(suc n-1)} k with (any? {n = n} (λ (x , _) → discreteℕ (x · k
                      (suc< (z<suc k)) (z<suc n-1) (snd (∣-untrunc |ddiv|))) ,
             snd (∣-untrunc |ddiv|)))
 
-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)
-
 HasFactor : (n k : ℕ) → Type
 HasFactor n k = (1 < k) × (k ∣ n)
 
 DecHF : ∀ {n} k → Dec (HasFactor n k)
-DecHF = DecProd Dec-1<n Dec-k∣n
+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
@@ -262,12 +251,8 @@ n≤! (suc n) = n≤n·pos (suc n) (n !) (0<factorial n)
     a∣n! : a ∣ (n !)
     a∣n! = ≤n∣n! a n (k , injSuc (sym (+-suc k a) ∙ k+sa=sn)) na=0
 
--- All and mapAll
+-- 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)
-
-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