diff --git a/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda b/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda
index 09a02f0e18..5b3f3c3351 100644
--- a/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda
+++ b/Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda
@@ -386,7 +386,7 @@ module Equiv-Properties
   lemmakk zero a = cong (base 0) (transportRefl a)
   lemmakk (suc k) a with (discreteℕ (suc k) (suc k)) | (discreteℕ k k)
   ... | yes p | yes q = cong₂ _add_
-                             (sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base (cong suc q) a))
+                             (sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base p a))
                              (lemmaSkk (suc k) a k ≤-refl)
                         ∙ +⊕HIT-IdR _
   ... | yes p | no ¬q = ⊥.rec (¬q refl)
diff --git a/Cubical/Algebra/Semilattice/Instances/NatMax.agda b/Cubical/Algebra/Semilattice/Instances/NatMax.agda
index 91e2f55689..6fb6ef8d46 100644
--- a/Cubical/Algebra/Semilattice/Instances/NatMax.agda
+++ b/Cubical/Algebra/Semilattice/Instances/NatMax.agda
@@ -35,8 +35,14 @@ isSemilattice maxSemilatticeStr = makeIsSemilattice isSetℕ maxAssoc maxRId max
   maxAssoc : (x y z : ℕ) → max x (max y z) ≡ max (max x y) z
   maxAssoc zero y z = refl
   maxAssoc (suc x) zero z = refl
-  maxAssoc (suc x) (suc y) zero = refl
-  maxAssoc (suc x) (suc y) (suc z) = cong suc (maxAssoc x y z)
+  maxAssoc (suc x) (suc y) zero = maxSuc ∙ cong (λ p → max p _) (sym (maxSuc {x} {y}))
+  maxAssoc (suc x) (suc y) (suc z) =
+    max (suc x) (max (suc y) (suc z)) ≡⟨ cong (max _) (maxSuc {y} {z}) ⟩
+    max (suc x) (suc (max y z))       ≡⟨ maxSuc ⟩
+    suc (max x (max y z))             ≡⟨ cong suc (maxAssoc x y z) ⟩
+    suc (max (max x y) z)             ≡⟨ sym maxSuc ⟩
+    max (suc (max x y)) (suc z)       ≡⟨ cong (λ p → max p _) (sym (maxSuc {x} {y})) ⟩
+    max (max (suc x) (suc y)) (suc z) ∎
 
   maxRId : (x : ℕ) → max x 0 ≡ x
   maxRId zero = refl
@@ -44,8 +50,7 @@ isSemilattice maxSemilatticeStr = makeIsSemilattice isSetℕ maxAssoc maxRId max
 
   maxIdem : (x : ℕ) → max x x ≡ x
   maxIdem zero = refl
-  maxIdem (suc x) = cong suc (maxIdem x)
-
+  maxIdem (suc x) = maxSuc ∙ cong suc (maxIdem x)
 
 
 --characterisation of inequality
@@ -54,13 +59,13 @@ open JoinSemilattice (ℕ , maxSemilatticeStr) renaming (_≤_ to _≤max_)
 ≤max→≤ℕ : ∀ x y → x ≤max y → x ≤ℕ y
 ≤max→≤ℕ zero y _ = zero-≤
 ≤max→≤ℕ (suc x) zero p = ⊥.rec (snotz p)
-≤max→≤ℕ (suc x) (suc y) p = let (k , q) = ≤max→≤ℕ x y (cong predℕ p) in
+≤max→≤ℕ (suc x) (suc y) p = let (k , q) = ≤max→≤ℕ x y (cong predℕ (sym maxSuc ∙ p)) in
                             k , +-suc k x ∙ cong suc q
 
 ≤ℕ→≤max :  ∀ x y → x ≤ℕ y → x ≤max y
 ≤ℕ→≤max zero y _ = refl
 ≤ℕ→≤max (suc x) zero p = ⊥.rec (¬-<-zero p)
-≤ℕ→≤max (suc x) (suc y) (k , p) = cong suc (≤ℕ→≤max x y (k , q))
+≤ℕ→≤max (suc x) (suc y) (k , p) = maxSuc ∙ cong suc (≤ℕ→≤max x y (k , q))
   where
   q : k +ℕ x ≡ y
   q = cong predℕ (sym (+-suc k x) ∙ p)
diff --git a/Cubical/Data/Nat/Base.agda b/Cubical/Data/Nat/Base.agda
index 12b21c4c86..545dbadb90 100644
--- a/Cubical/Data/Nat/Base.agda
+++ b/Cubical/Data/Nat/Base.agda
@@ -3,7 +3,7 @@ module Cubical.Data.Nat.Base where
 
 open import Agda.Builtin.Nat public
   using (zero; suc; _+_)
-  renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_)
+  renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_ ; _<_ to _<ᵇ_ ; _==_ to _≡ᵇ_)
 
 open import Cubical.Data.Nat.Literals public
 open import Cubical.Data.Bool.Base
diff --git a/Cubical/Data/Nat/Order.agda b/Cubical/Data/Nat/Order.agda
index 27562f06e3..9debbd67bc 100644
--- a/Cubical/Data/Nat/Order.agda
+++ b/Cubical/Data/Nat/Order.agda
@@ -10,6 +10,8 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum as ⊎
 
+open import Cubical.Data.Bool.Base hiding (_≟_)
+
 open import Cubical.Data.Nat.Base
 open import Cubical.Data.Nat.Properties
 
@@ -258,22 +260,59 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
 left-≤-max : m ≤ max m n
 left-≤-max {zero} {n} = zero-≤
 left-≤-max {suc m} {zero} = ≤-refl
-left-≤-max {suc m} {suc n} = suc-≤-suc left-≤-max
+left-≤-max {suc m} {suc n} = subst (_ ≤_) (sym maxSuc) $ suc-≤-suc $ left-≤-max {m} {n}
 
 right-≤-max : n ≤ max m n
 right-≤-max {zero} {m} = zero-≤
 right-≤-max {suc n} {zero} = ≤-refl
-right-≤-max {suc n} {suc m} = suc-≤-suc right-≤-max
+right-≤-max {suc n} {suc m} = subst (_ ≤_) (sym maxSuc) $ suc-≤-suc $ right-≤-max {n} {m}
 
 min-≤-left : min m n ≤ m
 min-≤-left {zero} {n} = ≤-refl
 min-≤-left {suc m} {zero} = zero-≤
-min-≤-left {suc m} {suc n} = suc-≤-suc min-≤-left
+min-≤-left {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-left {m} {n}
 
 min-≤-right : min m n ≤ n
 min-≤-right {zero} {n} = zero-≤
 min-≤-right {suc m} {zero} = ≤-refl
-min-≤-right {suc m} {suc n} = suc-≤-suc min-≤-right
+min-≤-right {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-right {m} {n}
+
+-- Boolean order relations and their conversions to/from ≤ and <
+
+_≤ᵇ_ : ℕ → ℕ → Bool
+m ≤ᵇ n = m <ᵇ suc n
+
+_≥ᵇ_ : ℕ → ℕ → Bool
+m ≥ᵇ n = n ≤ᵇ m
+
+_>ᵇ_ : ℕ → ℕ → Bool
+m >ᵇ n = n <ᵇ m
+
+private
+  ≤ᵇ-∸-+-cancel : ∀ m n → Bool→Type (m ≤ᵇ n) → (n ∸ m) + m ≡ n
+  ≤ᵇ-∸-+-cancel zero    zero    t = refl
+  ≤ᵇ-∸-+-cancel zero    (suc n) t = +-zero (suc n)
+  ≤ᵇ-∸-+-cancel (suc m) (suc n) t = +-suc (n ∸ m) m ∙ cong suc (≤ᵇ-∸-+-cancel m n t)
+
+<ᵇ→< : Bool→Type (m <ᵇ n) → m < n
+<ᵇ→< {m} {suc n} t .fst = n ∸ m
+<ᵇ→< {m} {suc n} t .snd =
+  n ∸ m + suc m   ≡⟨ +-suc (n ∸ m) m ⟩
+  suc (n ∸ m + m) ≡⟨ cong suc (≤ᵇ-∸-+-cancel m n t) ⟩
+  suc n           ∎
+
+<→<ᵇ : m < n → Bool→Type (m <ᵇ n)
+<→<ᵇ {m}     {zero}  m<0   = ¬-<-zero m<0
+<→<ᵇ {zero}  {suc n} 0<sn  = tt
+<→<ᵇ {suc m} {suc n} sm<sn = <→<ᵇ (pred-≤-pred sm<sn)
+
+≤ᵇ→≤ : Bool→Type (m ≤ᵇ n) → m ≤ n
+≤ᵇ→≤ {zero}  {n}     t = zero-≤
+≤ᵇ→≤ {suc m} {suc n} t = <ᵇ→< t
+
+≤→≤ᵇ : m ≤ n → Bool→Type (m ≤ᵇ n)
+≤→≤ᵇ {zero}  {n} 0≤n  = tt
+≤→≤ᵇ {suc m} {n} sm≤n = <→<ᵇ sm≤n
 
 ≤Dec : ∀ m n → Dec (m ≤ n)
 ≤Dec zero n = yes (n , +-zero _)
@@ -296,11 +335,27 @@ Trichotomy-suc (lt m<n) = lt (suc-≤-suc m<n)
 Trichotomy-suc (eq m=n) = eq (cong suc m=n)
 Trichotomy-suc (gt n<m) = gt (suc-≤-suc n<m)
 
+private
+  ∸→>ᵇ : ∀ m n → caseNat ⊥.⊥ Unit (m ∸ n) → Bool→Type (m >ᵇ n)
+  ∸→>ᵇ (suc m) zero    t = tt
+  ∸→>ᵇ (suc m) (suc n) t = ∸→>ᵇ m n t
+
 _≟_ : ∀ m n → Trichotomy m n
-zero ≟ zero = eq refl
-zero ≟ suc n = lt (n , +-comm n 1)
-suc m ≟ zero = gt (m , +-comm m 1)
-suc m ≟ suc n = Trichotomy-suc (m ≟ n)
+m ≟ n with m ∸ n UsingEq | n ∸ m UsingEq
+... | zero  , p | zero  , q = eq (∸≡0→≡ p q)
+... | zero  , p | suc _ , q = lt (<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
+... | suc _ , p | zero  , q = gt (<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)
+... | suc _ , p | suc _ , q = ⊥.rec $ ¬m<m {m} $ <-trans
+  (<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
+  (<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)
+
+--  Alternative version of ≟, defined without builtin primitives
+
+_≟'_ : ∀ m n → Trichotomy m n
+zero ≟' zero = eq refl
+zero ≟' suc n = lt (n , +-comm n 1)
+suc m ≟' zero = gt (m , +-comm m 1)
+suc m ≟' suc n = Trichotomy-suc (m ≟' n)
 
 Dichotomyℕ : ∀ (n m : ℕ) → (n ≤ m) ⊎ (n > m)
 Dichotomyℕ n m with (n ≟ m)
@@ -331,7 +386,10 @@ splitℕ-< m n with m ≟ n
 <-split : m < suc n → (m < n) ⊎ (m ≡ n)
 <-split {n = zero} = inr ∘ snd ∘ m+n≡0→m≡0×n≡0 ∘ snd ∘ pred-≤-pred
 <-split {zero} {suc n} = λ _ → inl (suc-≤-suc zero-≤)
-<-split {suc m} {suc n} = ⊎.map suc-≤-suc (cong suc) ∘ <-split ∘ pred-≤-pred
+<-split {suc m} {suc n} sm<ssn with m ≟ n
+... | lt m<n = inl (suc-≤-suc m<n)
+... | eq m≡n = inr (cong suc m≡n)
+... | gt n<m = ⊥.rec $ ¬m<m {suc (suc n)} $ ≤-trans (suc-≤-suc (suc-≤-suc n<m)) sm<ssn
 
 ≤-split : m ≤ n → (m < n) ⊎ (m ≡ n)
 ≤-split p = <-split (suc-≤-suc p)
diff --git a/Cubical/Data/Nat/Properties.agda b/Cubical/Data/Nat/Properties.agda
index 2590a016bc..047cae1ed0 100644
--- a/Cubical/Data/Nat/Properties.agda
+++ b/Cubical/Data/Nat/Properties.agda
@@ -12,6 +12,8 @@ open import Cubical.Data.Empty as ⊥
 open import Cubical.Data.Sigma
 open import Cubical.Data.Sum.Base
 
+open import Cubical.Data.Bool.Base
+
 open import Cubical.Relation.Nullary
 
 private
@@ -21,24 +23,44 @@ private
 min : ℕ → ℕ → ℕ
 min zero m = zero
 min (suc n) zero = zero
-min (suc n) (suc m) = suc (min n m)
+min (suc n) (suc m) with n <ᵇ m
+... | false = suc m
+... | true  = suc n
+
+minSuc : min (suc n) (suc m) ≡ suc (min n m)
+minSuc {zero} {zero} = refl
+minSuc {zero} {suc m} = refl
+minSuc {suc n} {zero} = refl
+minSuc {suc n} {suc m} with suc n <ᵇ suc m
+... | false = refl
+... | true  = refl
 
 minComm : (n m : ℕ) → min n m ≡ min m n
 minComm zero zero = refl
 minComm zero (suc m) = refl
 minComm (suc n) zero = refl
-minComm (suc n) (suc m) = cong suc (minComm n m)
+minComm (suc n) (suc m) = minSuc ∙∙ cong suc (minComm n m) ∙∙ sym minSuc
 
 max : ℕ → ℕ → ℕ
 max zero m = m
 max (suc n) zero = suc n
-max (suc n) (suc m) = suc (max n m)
+max (suc n) (suc m) with n <ᵇ m
+... | false = suc n
+... | true  = suc m
+
+maxSuc : max (suc n) (suc m) ≡ suc (max n m)
+maxSuc {zero} {zero} = refl
+maxSuc {zero} {suc m} = refl
+maxSuc {suc n} {zero} = refl
+maxSuc {suc n} {suc m} with suc n <ᵇ suc m
+... | false = refl
+... | true  = refl
 
 maxComm : (n m : ℕ) → max n m ≡ max m n
 maxComm zero zero = refl
 maxComm zero (suc m) = refl
 maxComm (suc n) zero = refl
-maxComm (suc n) (suc m) = cong suc (maxComm n m)
+maxComm (suc n) (suc m) = maxSuc ∙∙ cong suc (maxComm n m) ∙∙ sym maxSuc
 
 znots : ¬ (0 ≡ suc n)
 znots eq = subst (caseNat ℕ ⊥) eq 0
@@ -122,14 +144,22 @@ decodeℕ (suc n) (suc m) = λ r → cong suc (decodeℕ n m r)
     retr : (n m : ℕ) → (p : n ≡ m) → decodeℕ n m (compute-eqℕ n m p) ≡ p
     retr n m p = J (λ m p → decodeℕ n m (compute-eqℕ n m p) ≡ p) (reflRetr n) p
 
+-- Conversions between boolean equality (≡ᵇ) and path equality (≡)
+
+≡ᵇ→≡ : Bool→Type (m ≡ᵇ n) → m ≡ n
+≡ᵇ→≡ {zero}  {zero}  t = refl
+≡ᵇ→≡ {suc m} {suc n} t = cong suc (≡ᵇ→≡ t)
+
+≡→≡ᵇ : m ≡ n → Bool→Type (m ≡ᵇ n)
+≡→≡ᵇ {zero}  {zero}  _ = tt
+≡→≡ᵇ {zero}  {suc n} p = ⊥.rec (znots p)
+≡→≡ᵇ {suc m} {zero}  p = ⊥.rec (snotz p)
+≡→≡ᵇ {suc m} {suc n} p = ≡→≡ᵇ {m} {n} (cong predℕ p)
 
 discreteℕ : Discrete ℕ
-discreteℕ zero zero = yes refl
-discreteℕ zero (suc n) = no znots
-discreteℕ (suc m) zero = no snotz
-discreteℕ (suc m) (suc n) with discreteℕ m n
-... | yes p = yes (cong suc p)
-... | no p = no (λ x → p (injSuc x))
+discreteℕ m n with m ≡ᵇ n UsingEq
+... | false , p = no  (subst Bool→Type p ∘ ≡→≡ᵇ)
+... | true  , p = yes (≡ᵇ→≡ (subst Bool→Type (sym p) tt))
 
 separatedℕ : Separated ℕ
 separatedℕ = Discrete→Separated discreteℕ
@@ -270,6 +300,12 @@ n∸n (suc n) = n∸n n
 ∸-distribʳ zero    (suc n) k = sym (zero∸ (k + n · k))
 ∸-distribʳ (suc m) (suc n) k = ∸-distribʳ m n k ∙ sym (∸-cancelˡ k (m · k) (n · k))
 
+∸≡0→≡ : m ∸ n ≡ 0 → n ∸ m ≡ 0 → m ≡ n
+∸≡0→≡ {zero}  {zero}  _ _ = refl
+∸≡0→≡ {zero}  {suc n} _ q = ⊥.rec (snotz q)
+∸≡0→≡ {suc m} {zero}  p _ = ⊥.rec (snotz p)
+∸≡0→≡ {suc m} {suc n} p q = cong suc (∸≡0→≡ {m} {n} p q)
+
 infix 6 _!
 infix 7 _choose_
 
diff --git a/Cubical/Foundations/Prelude.agda b/Cubical/Foundations/Prelude.agda
index a9454e5875..260be6bfb9 100644
--- a/Cubical/Foundations/Prelude.agda
+++ b/Cubical/Foundations/Prelude.agda
@@ -498,6 +498,20 @@ isContrSinglP A a .fst = _ , transport-filler (λ i → A i) a
 isContrSinglP A a .snd (x , p) i =
   _ , λ j → fill A (λ j → λ {(i = i0) → transport-filler (λ i → A i) a j; (i = i1) → p j}) (inS a) j
 
+-- Helpers for carrying equalities into with-abstractions
+-- see `discreteℕ` in Data.Nat.Properties for an example of usage
+
+infixl 0 _UsingEq
+infixl 0 _i0:>_UsingEqP
+
+-- Similar to `inspect`, but more convenient when `a` is not a function
+-- application, or when the applied function is not relevant
+_UsingEq : (a : A) → singl a
+a UsingEq = isContrSingl a .fst
+
+_i0:>_UsingEqP : (A : I → Type ℓ) (a : A i0) → singlP A a
+A i0:> a UsingEqP = isContrSinglP A a .fst
+
 -- Higher cube types
 
 SquareP :
diff --git a/Cubical/HITs/Truncation/Properties.agda b/Cubical/HITs/Truncation/Properties.agda
index 1b111745c0..f812a2efa4 100644
--- a/Cubical/HITs/Truncation/Properties.agda
+++ b/Cubical/HITs/Truncation/Properties.agda
@@ -213,14 +213,23 @@ isOfHLevelMin→isOfHLevel {n = suc n} {m = zero} h = (isContr→isOfHLevel (suc
 isOfHLevelMin→isOfHLevel {A = A} {n = suc n} {m = suc m} h =
     subst (λ x → isOfHLevel x A) (helper n m)
           (isOfHLevelPlus (suc n ∸ (suc (min n m))) h)
-  , subst (λ x → isOfHLevel x A) ((λ i → m ∸ (minComm n m i) + suc (minComm n m i)) ∙ helper m n)
+  , subst (λ x → isOfHLevel x A) ((λ i → m ∸ (minComm n m i) + (minComm (suc n) (suc m) i)) ∙ helper m n)
           (isOfHLevelPlus (suc m ∸ (suc (min n m))) h)
   where
-  helper : (n m : ℕ) → n ∸ min n m + suc (min n m) ≡ suc n
+  helper : (n m : ℕ) → n ∸ min n m + min (suc n) (suc m) ≡ suc n
   helper zero zero = refl
   helper zero (suc m) = refl
   helper (suc n) zero = cong suc (+-comm n 1)
-  helper (suc n) (suc m) = +-suc _ _ ∙ cong suc (helper n m)
+  helper (suc n) (suc m) =
+    suc n ∸ min (suc n) (suc m) + min (suc (suc n)) (suc (suc m)) ≡⟨ step0 ⟩
+    suc n ∸ suc (min n m) + suc (min (suc n) (suc m))             ≡⟨⟩
+    n ∸ min n m + suc (min (suc n) (suc m))                       ≡⟨ step1 ⟩
+    suc (n ∸ min n m + min (suc n) (suc m))                       ≡⟨ step2 ⟩
+    suc (suc n)                                                   ∎
+    where
+      step0 = cong₂ (λ p → suc n ∸ p +_) (minSuc {n}) minSuc
+      step1 = +-suc _ _
+      step2 = cong suc (helper n m)
 
 ΣTruncElim : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {n m : ℕ}
              {B : (x : ∥ A ∥ n) → Type ℓ'}
@@ -228,9 +237,9 @@ isOfHLevelMin→isOfHLevel {A = A} {n = suc n} {m = suc m} h =
              → ((x : (Σ[ a ∈ (∥ A ∥ n) ] (∥ B a ∥ m))) → isOfHLevel (min n m) (C x))
              → ((a : A) (b : B (∣ a ∣ₕ)) → C (∣ a ∣ₕ , ∣ b ∣ₕ))
              → (x : (Σ[ a ∈ (∥ A ∥ n) ] (∥ B a ∥ m))) → C x
-ΣTruncElim hB g (a , b) =
+ΣTruncElim {n = n} hB g (a , b) =
   elim (λ x → isOfHLevelΠ _ λ b → isOfHLevelMin→isOfHLevel (hB (x , b)) .fst )
-       (λ a → elim (λ _ → isOfHLevelMin→isOfHLevel (hB (∣ a ∣ₕ , _)) .snd) λ b → g a b)
+       (λ a → elim (λ _ → isOfHLevelMin→isOfHLevel {n = n} (hB (∣ a ∣ₕ , _)) .snd) λ b → g a b)
        a b
 
 truncIdempotentIso : (n : ℕ) → isOfHLevel n A → Iso (∥ A ∥ n) A