diff --git a/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md b/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
index 52541dc0ab..e02ea3e094 100644
--- a/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/based-strong-induction-natural-numbers.lagda.md
@@ -53,7 +53,7 @@ satisfying
 
 ```agda
 based-□-≤-ℕ : {l : Level} (k : ℕ) → (ℕ → UU l) → ℕ → UU l
-based-□-≤-ℕ k P n = (m : ℕ) → (k ≤-ℕ m) → (m ≤-ℕ n) → P m
+based-□-≤-ℕ k P n = (m : ℕ) → k ≤-ℕ m → m ≤-ℕ n → P m
 
 η-based-□-≤-ℕ :
   {l : Level} (k : ℕ) {P : ℕ → UU l} → ((n : ℕ) → k ≤-ℕ n → P n) →
@@ -61,7 +61,8 @@ based-□-≤-ℕ k P n = (m : ℕ) → (k ≤-ℕ m) → (m ≤-ℕ n) → P m
 η-based-□-≤-ℕ k f n N m M p = f m M
 
 ε-based-□-≤-ℕ :
-  {l : Level} (k : ℕ) {P : ℕ → UU l} → ((n : ℕ) → k ≤-ℕ n → based-□-≤-ℕ k P n) →
+  {l : Level} (k : ℕ) {P : ℕ → UU l} →
+  ((n : ℕ) → k ≤-ℕ n → based-□-≤-ℕ k P n) →
   ((n : ℕ) → k ≤-ℕ n → P n)
 ε-based-□-≤-ℕ k f n N = f n N n N (refl-leq-ℕ n)
 ```
@@ -128,7 +129,7 @@ cases-eq-succ-based-strong-ind-ℕ :
   {l : Level} (k : ℕ) (P : ℕ → UU l)
   (pS : (x : ℕ) → k ≤-ℕ x → based-□-≤-ℕ k P x → P (succ-ℕ x)) →
   (n : ℕ) (N : k ≤-ℕ n) (f : based-□-≤-ℕ k P n) (M : k ≤-ℕ succ-ℕ n)
-  (c : (leq-ℕ (succ-ℕ n) n) + (succ-ℕ n ＝ succ-ℕ n)) →
+  (c : (succ-ℕ n ≤-ℕ n) + (succ-ℕ n ＝ succ-ℕ n)) →
   cases-succ-based-strong-ind-ℕ k P pS n N f (succ-ℕ n) M c ＝ pS n N f
 cases-eq-succ-based-strong-ind-ℕ k P pS n N f M (inl H) =
   ex-falso (neg-succ-leq-ℕ n H)
@@ -141,7 +142,7 @@ eq-succ-based-strong-ind-ℕ :
   {l : Level} (k : ℕ) (P : ℕ → UU l)
   (pS : (x : ℕ) → k ≤-ℕ x → (based-□-≤-ℕ k P x) → P (succ-ℕ x)) →
   (n : ℕ) (N : k ≤-ℕ n) (f : based-□-≤-ℕ k P n) (M : k ≤-ℕ succ-ℕ n)
-  (H : leq-ℕ (succ-ℕ n) (succ-ℕ n)) →
+  (H : succ-ℕ n ≤-ℕ succ-ℕ n) →
   succ-based-strong-ind-ℕ k P pS n N f (succ-ℕ n) M H ＝ pS n N f
 eq-succ-based-strong-ind-ℕ k P pS n N f M H =
   cases-eq-succ-based-strong-ind-ℕ k P pS n N f M (cases-leq-succ-ℕ H)
diff --git a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
index cb14d6fcfd..f0f3b7f70d 100644
--- a/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
+++ b/src/elementary-number-theory/bezouts-lemma-integers.lagda.md
@@ -46,100 +46,55 @@ bezouts-lemma-eqn-to-int :
     ( abs-ℤ
       ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H) *ℤ y))
 bezouts-lemma-eqn-to-int x y H =
-  equational-reasoning
-    nat-gcd-ℤ x y
-    ＝ dist-ℕ
-      ( (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H) *ℕ (abs-ℤ x))
-      ( (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H) *ℕ (abs-ℤ y))
-      by (inv (bezouts-lemma-eqn-ℕ (abs-ℤ x) (abs-ℤ y) H))
-    ＝ dist-ℕ
-        ( mul-ℕ
-          ( abs-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H)))
-          ( abs-ℤ x))
+  ( inv (bezouts-lemma-eqn-ℕ (abs-ℤ x) (abs-ℤ y) H)) ∙
+  ( ap
+    ( λ K →
+      dist-ℕ
+        ( K *ℕ (abs-ℤ x))
         ( mul-ℕ
           ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)
-          ( abs-ℤ y))
-      by
-        ( ap
-          ( λ K →
-            dist-ℕ
-              ( K *ℕ (abs-ℤ x))
-              ( mul-ℕ
-                ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)
-                ( abs-ℤ y)))
-          ( inv
-            ( abs-int-ℕ
-              ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))))
-    ＝ dist-ℕ
+          ( abs-ℤ y)))
+    ( inv
+      ( abs-int-ℕ
+        ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H)))) ∙
+  ( ap
+    ( λ K →
+      dist-ℕ
         ( mul-ℕ
           ( abs-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H)))
+            ( int-ℕ
+              ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H)))
           ( abs-ℤ x))
+        ( K *ℕ (abs-ℤ y)))
+    ( inv
+      ( abs-int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))) ∙
+  ( ap
+    ( λ K →
+      dist-ℕ
+        ( K)
         ( mul-ℕ
           ( abs-ℤ
-            ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))
-          ( abs-ℤ y))
-      by
-        ( ap
-          ( λ K →
-            dist-ℕ
-              ( mul-ℕ
-                ( abs-ℤ
-                  ( int-ℕ
-                    ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H)))
-                ( abs-ℤ x))
-              ( K *ℕ (abs-ℤ y)))
-        (inv
-          ( abs-int-ℕ
-            ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H))))
-    ＝ dist-ℕ
-        ( abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
-            ( x)))
-        ( mul-ℕ
-          ( abs-ℤ
-            ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))
-          ( abs-ℤ y))
-      by
-        ( ap
-          ( λ K →
-            dist-ℕ
-              ( K)
-              ( mul-ℕ
-                ( abs-ℤ
-                  ( int-ℕ
-                    ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))
-                ( abs-ℤ y)))
-          ( inv
-            ( multiplicative-abs-ℤ
-              ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
-              ( x))))
-    ＝ dist-ℕ
-        ( abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
-            ( x)))
-        ( abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H))
-            ( y)))
-      by
-        ( ap
-          ( dist-ℕ
-            ( abs-ℤ
-              ( mul-ℤ
-                ( int-ℕ
-                  ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
-                ( x))))
-          ( inv
-            ( multiplicative-abs-ℤ
-              ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H))
-              ( y))))
+            ( int-ℕ
+              ( minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H)))
+          ( abs-ℤ y)))
+    ( inv
+      ( multiplicative-abs-ℤ
+        ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
+        ( x)))) ∙
+  ( ap
+    ( dist-ℕ
+      ( abs-ℤ
+        ( mul-ℤ
+          ( int-ℕ
+            ( minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) H))
+          ( x))))
+    ( inv
+      ( multiplicative-abs-ℤ
+        ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) H))
+        ( y))))
 
 refactor-pos-cond :
-  (x y : ℤ) → (H : is-positive-ℤ x) → (K : is-positive-ℤ y) →
+  (x y : ℤ) (H : is-positive-ℤ x) (K : is-positive-ℤ y) →
   is-nonzero-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y))
 refactor-pos-cond x y H _ =
   is-nonzero-abs-ℤ x H ∘ is-zero-left-is-zero-add-ℕ (abs-ℤ x) (abs-ℤ y)
@@ -164,30 +119,16 @@ bezouts-lemma-refactor-hypotheses :
             ( refactor-pos-cond x y H K)))
         ( y)))
 bezouts-lemma-refactor-hypotheses x y H K =
-  equational-reasoning
-    nat-gcd-ℤ x y
-    ＝ dist-ℕ
-        ( abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P))
-            ( x)))
-        ( abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P))
-            ( y)))
-      by bezouts-lemma-eqn-to-int x y P
-    ＝ dist-ℤ
-        ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ x)
-        ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P) *ℤ y)
-      by
-        dist-abs-ℤ
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P))
-            ( x))
-          ( mul-ℤ
-            ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P))
-            ( y))
-        x-product-nonneg y-product-nonneg
+  bezouts-lemma-eqn-to-int x y P ∙
+  dist-abs-ℤ
+    ( mul-ℤ
+      ( int-ℕ (minimal-positive-distance-x-coeff (abs-ℤ x) (abs-ℤ y) P))
+      ( x))
+    ( mul-ℤ
+      ( int-ℕ (minimal-positive-distance-y-coeff (abs-ℤ x) (abs-ℤ y) P))
+      ( y))
+    ( x-product-nonneg)
+    ( y-product-nonneg)
   where
   P : is-nonzero-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y))
   P = (refactor-pos-cond x y H K)
@@ -229,37 +170,24 @@ bezouts-lemma-pos-ints x y H K =
   pr1 (pr2 (sx-ty-nonneg-case-split (inl pos))) = neg-ℤ t
   pr2 (pr2 (sx-ty-nonneg-case-split (inl pos))) =
     inv
-    ( equational-reasoning
-        gcd-ℤ x y
-        ＝ int-ℕ (abs-ℤ ((s *ℤ x) -ℤ (t *ℤ y)))
-          by ap int-ℕ (bezouts-lemma-refactor-hypotheses x y H K)
-        ＝ (s *ℤ x) -ℤ (t *ℤ y)
-          by int-abs-is-nonnegative-ℤ ((s *ℤ x) -ℤ (t *ℤ y)) pos
-        ＝ (s *ℤ x) +ℤ ((neg-ℤ t) *ℤ y)
-          by ap ((s *ℤ x) +ℤ_) (inv (left-negative-law-mul-ℤ t y)))
+    ( ( ap int-ℕ (bezouts-lemma-refactor-hypotheses x y H K)) ∙
+      ( int-abs-is-nonnegative-ℤ ((s *ℤ x) -ℤ (t *ℤ y)) pos) ∙
+      ( ap ((s *ℤ x) +ℤ_) (inv (left-negative-law-mul-ℤ t y))))
 
   pr1 (sx-ty-nonneg-case-split (inr neg)) = neg-ℤ s
   pr1 (pr2 (sx-ty-nonneg-case-split (inr neg))) = t
   pr2 (pr2 (sx-ty-nonneg-case-split (inr neg))) =
     inv
-      ( equational-reasoning
-          gcd-ℤ x y
-          ＝ int-ℕ (abs-ℤ ((s *ℤ x) -ℤ (t *ℤ y)))
-            by ap int-ℕ (bezouts-lemma-refactor-hypotheses x y H K)
-          ＝ int-ℕ (abs-ℤ (neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y))))
-            by ap (int-ℕ) (inv (abs-neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y))))
-          ＝ neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y))
-            by
-              int-abs-is-nonnegative-ℤ
-                ( neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y)))
-                ( neg)
-          ＝ (neg-ℤ (s *ℤ x)) +ℤ (neg-ℤ (neg-ℤ (t *ℤ y)))
-            by distributive-neg-add-ℤ (s *ℤ x) (neg-ℤ (t *ℤ y))
-          ＝ ((neg-ℤ s) *ℤ x) +ℤ (neg-ℤ (neg-ℤ (t *ℤ y)))
-            by ap (_+ℤ (neg-ℤ (neg-ℤ (t *ℤ y))))
-              (inv (left-negative-law-mul-ℤ s x))
-          ＝ ((neg-ℤ s) *ℤ x) +ℤ (t *ℤ y)
-            by ap (((neg-ℤ s) *ℤ x) +ℤ_) (neg-neg-ℤ (t *ℤ y)))
+      ( ( ap int-ℕ (bezouts-lemma-refactor-hypotheses x y H K)) ∙
+        ( ap (int-ℕ) (inv (abs-neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y))))) ∙
+        ( int-abs-is-nonnegative-ℤ
+          ( neg-ℤ ((s *ℤ x) -ℤ (t *ℤ y)))
+          ( neg)) ∙
+        ( distributive-neg-add-ℤ (s *ℤ x) (neg-ℤ (t *ℤ y))) ∙
+        ( ap
+          ( _+ℤ (neg-ℤ (neg-ℤ (t *ℤ y))))
+          ( inv (left-negative-law-mul-ℤ s x))) ∙
+        ( ap (((neg-ℤ s) *ℤ x) +ℤ_) (neg-neg-ℤ (t *ℤ y))))
 
 bezouts-lemma-ℤ :
   (x y : ℤ) → Σ ℤ (λ s → Σ ℤ (λ t → (s *ℤ x) +ℤ (t *ℤ y) ＝ gcd-ℤ x y))
@@ -281,44 +209,27 @@ bezouts-lemma-ℤ (inl x) (inl y) = pair (neg-ℤ s) (pair (neg-ℤ t) eqn)
     ((neg-ℤ s) *ℤ (inl x)) +ℤ ((neg-ℤ t) *ℤ (inl y)) ＝
     gcd-ℤ (inl x) (inl y)
   eqn =
-    equational-reasoning
-      ( (neg-ℤ s) *ℤ (neg-ℤ (inr (inr x)))) +ℤ
-      ( (neg-ℤ t) *ℤ (neg-ℤ (inr (inr y))))
-      ＝ (s *ℤ (inr (inr x))) +ℤ ((neg-ℤ t) *ℤ (neg-ℤ (inr (inr y))))
-        by
-          ( ap
-            ( _+ℤ ((neg-ℤ t) *ℤ (neg-ℤ (inr (inr y)))))
-            ( double-negative-law-mul-ℤ s (inr (inr x))))
-      ＝ (s *ℤ (inr (inr x))) +ℤ (t *ℤ (inr (inr y)))
-        by
-          ( ap
-            ( (s *ℤ (inr (inr x))) +ℤ_)
-            ( double-negative-law-mul-ℤ t (inr (inr y))))
-      ＝ gcd-ℤ (inr (inr x)) (inr (inr y))
-        by pr2 (pr2 (pos-bezout))
-      ＝ gcd-ℤ (inl x) (inr (inr y))
-        by ap (λ M → (int-ℕ (gcd-ℕ M (succ-ℕ y)))) (abs-neg-ℤ (inr (inr x)))
-      ＝ gcd-ℤ (inl x) (inl y)
-        by ap (λ M → (int-ℕ (gcd-ℕ (succ-ℕ x) M))) (abs-neg-ℤ (inr (inr y)))
+    ( ap
+      ( _+ℤ ((neg-ℤ t) *ℤ (neg-ℤ (inr (inr y)))))
+      ( double-negative-law-mul-ℤ s (inr (inr x)))) ∙
+    ( ap
+      ( (s *ℤ (inr (inr x))) +ℤ_)
+      ( double-negative-law-mul-ℤ t (inr (inr y)))) ∙
+    ( pr2 (pr2 (pos-bezout))) ∙
+    ( ap (λ M → (int-ℕ (gcd-ℕ M (succ-ℕ y)))) (abs-neg-ℤ (inr (inr x)))) ∙
+    ( ap (λ M → (int-ℕ (gcd-ℕ (succ-ℕ x) M))) (abs-neg-ℤ (inr (inr y))))
 bezouts-lemma-ℤ (inl x) (inr (inl star)) = pair neg-one-ℤ (pair one-ℤ eqn)
   where
   eqn :
     (neg-one-ℤ *ℤ (inl x)) +ℤ (one-ℤ *ℤ (inr (inl star))) ＝
     gcd-ℤ (inl x) (inr (inl star))
   eqn =
-    equational-reasoning
-      (neg-one-ℤ *ℤ (inl x)) +ℤ (one-ℤ *ℤ (inr (inl star)))
-      ＝ (inr (inr x)) +ℤ (one-ℤ *ℤ (inr (inl star)))
-        by
-          ap
-            ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
-            ( inv (is-left-mul-neg-one-neg-ℤ (inl x)))
-      ＝ (inr (inr x)) +ℤ zero-ℤ
-        by ap ((inr (inr x)) +ℤ_) (right-zero-law-mul-ℤ one-ℤ)
-      ＝ int-ℕ (abs-ℤ (inl x))
-        by right-unit-law-add-ℤ (inr (inr x))
-      ＝ gcd-ℤ (inl x) zero-ℤ
-        by inv (is-id-is-gcd-zero-ℤ' {inl x} {gcd-ℤ (inl x) zero-ℤ} refl)
+    ( ap
+      ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
+      ( inv (is-left-mul-neg-one-neg-ℤ (inl x)))) ∙
+    ( ap ((inr (inr x)) +ℤ_) (right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( right-unit-law-add-ℤ (inr (inr x))) ∙
+    ( inv (is-id-is-gcd-zero-ℤ' {inl x} {gcd-ℤ (inl x) zero-ℤ} refl))
 bezouts-lemma-ℤ (inl x) (inr (inr y)) = pair (neg-ℤ s) (pair t eqn)
   where
   pos-bezout :
@@ -337,74 +248,50 @@ bezouts-lemma-ℤ (inl x) (inr (inr y)) = pair (neg-ℤ s) (pair t eqn)
     ((neg-ℤ s) *ℤ (inl x)) +ℤ (t *ℤ (inr (inr y))) ＝
     gcd-ℤ (inl x) (inr (inr y))
   eqn =
-    equational-reasoning
-      ((neg-ℤ s) *ℤ (neg-ℤ (inr (inr x)))) +ℤ (t *ℤ (inr (inr y)))
-      ＝ (s *ℤ (inr (inr x))) +ℤ (t *ℤ (inr (inr y)))
-        by ap (_+ℤ (t *ℤ (inr (inr y))))
-          (double-negative-law-mul-ℤ s (inr (inr x)))
-      ＝ gcd-ℤ (inr (inr x)) (inr (inr y))
-        by pr2 (pr2 (pos-bezout))
-      ＝ gcd-ℤ (inl x) (inr (inr y))
-        by ap (λ M → (int-ℕ (gcd-ℕ M (succ-ℕ y)))) (abs-neg-ℤ (inr (inr x)))
+    ( ap
+      ( _+ℤ (t *ℤ (inr (inr y))))
+      ( double-negative-law-mul-ℤ s (inr (inr x)))) ∙
+    ( pr2 (pr2 (pos-bezout))) ∙
+    ( ap (λ M → (int-ℕ (gcd-ℕ M (succ-ℕ y)))) (abs-neg-ℤ (inr (inr x))))
 bezouts-lemma-ℤ (inr (inl star)) (inl y) = pair one-ℤ (pair neg-one-ℤ eqn)
   where
   eqn :
     (one-ℤ *ℤ (inr (inl star))) +ℤ (neg-one-ℤ *ℤ (inl y)) ＝
     gcd-ℤ (inr (inl star)) (inl y)
   eqn =
-    equational-reasoning
-      (one-ℤ *ℤ (inr (inl star))) +ℤ (neg-one-ℤ *ℤ (inl y))
-      ＝ (one-ℤ *ℤ (inr (inl star))) +ℤ (inr (inr y))
-        by
-          ap
-            ( (one-ℤ *ℤ (inr (inl star))) +ℤ_)
-            ( inv (is-left-mul-neg-one-neg-ℤ (inl y)))
-      ＝ zero-ℤ +ℤ (inr (inr y))
-        by ap (_+ℤ (inr (inr y))) (right-zero-law-mul-ℤ one-ℤ)
-      ＝ int-ℕ (abs-ℤ (inl y))
-        by left-unit-law-add-ℤ (inr (inr y))
-      ＝ gcd-ℤ zero-ℤ (inl y)
-        by inv (is-id-is-gcd-zero-ℤ {inl y} {gcd-ℤ zero-ℤ (inl y)} refl)
+    ( ap
+      ( (one-ℤ *ℤ (inr (inl star))) +ℤ_)
+      ( inv (is-left-mul-neg-one-neg-ℤ (inl y)))) ∙
+    ( ap (_+ℤ (inr (inr y))) (right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( left-unit-law-add-ℤ (inr (inr y))) ∙
+    ( inv (is-id-is-gcd-zero-ℤ {inl y} {gcd-ℤ zero-ℤ (inl y)} refl))
 bezouts-lemma-ℤ (inr (inl star)) (inr (inl star)) = pair one-ℤ (pair one-ℤ eqn)
   where
   eqn :
     (one-ℤ *ℤ (inr (inl star))) +ℤ (one-ℤ *ℤ (inr (inl star))) ＝
     gcd-ℤ zero-ℤ zero-ℤ
   eqn =
-    equational-reasoning
-      (one-ℤ *ℤ (inr (inl star))) +ℤ (one-ℤ *ℤ (inr (inl star)))
-      ＝ zero-ℤ +ℤ (one-ℤ *ℤ (inr (inl star)))
-        by
-          ap
-            ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
-            ( right-zero-law-mul-ℤ one-ℤ)
-      ＝ zero-ℤ +ℤ zero-ℤ
-        by ap (zero-ℤ +ℤ_) (right-zero-law-mul-ℤ one-ℤ)
-      ＝ gcd-ℤ zero-ℤ zero-ℤ
-        by inv (is-zero-gcd-ℤ zero-ℤ zero-ℤ refl refl)
+    ( ap
+      ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
+      ( right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( ap (zero-ℤ +ℤ_) (right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( inv (is-zero-gcd-ℤ zero-ℤ zero-ℤ refl refl))
 bezouts-lemma-ℤ (inr (inl star)) (inr (inr y)) = pair one-ℤ (pair one-ℤ eqn)
   where
   eqn :
     (one-ℤ *ℤ (inr (inl star))) +ℤ (one-ℤ *ℤ (inr (inr y))) ＝
     gcd-ℤ (inr (inl star)) (inr (inr y))
   eqn =
-    equational-reasoning
-      (one-ℤ *ℤ (inr (inl star))) +ℤ (one-ℤ *ℤ (inr (inr y)))
-      ＝ (one-ℤ *ℤ (inr (inl star))) +ℤ (inr (inr y))
-        by ap
-          ( (one-ℤ *ℤ (inr (inl star))) +ℤ_)
-          ( inv (left-unit-law-mul-ℤ (inr (inr y))))
-      ＝ zero-ℤ +ℤ (inr (inr y))
-        by ap (_+ℤ (inr (inr y))) (right-zero-law-mul-ℤ one-ℤ)
-      ＝ int-ℕ (abs-ℤ (inr (inr y)))
-        by left-unit-law-add-ℤ (inr (inr y))
-      ＝ gcd-ℤ zero-ℤ (inr (inr y))
-        by
-          inv
-            ( is-id-is-gcd-zero-ℤ
-              { inr (inr y)}
-              { gcd-ℤ zero-ℤ (inr (inr y))}
-              ( refl))
+    ( ap
+      ( (one-ℤ *ℤ (inr (inl star))) +ℤ_)
+      ( inv (left-unit-law-mul-ℤ (inr (inr y))))) ∙
+    ( ap (_+ℤ (inr (inr y))) (right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( left-unit-law-add-ℤ (inr (inr y))) ∙
+    ( inv
+      ( is-id-is-gcd-zero-ℤ
+        { inr (inr y)}
+        { gcd-ℤ zero-ℤ (inr (inr y))}
+        ( refl)))
 bezouts-lemma-ℤ (inr (inr x)) (inl y) = pair s (pair (neg-ℤ t) eqn)
   where
   pos-bezout :
@@ -423,39 +310,27 @@ bezouts-lemma-ℤ (inr (inr x)) (inl y) = pair s (pair (neg-ℤ t) eqn)
     (s *ℤ (inr (inr x))) +ℤ ((neg-ℤ t) *ℤ (inl y)) ＝
     gcd-ℤ (inr (inr x)) (inl y)
   eqn =
-    equational-reasoning
-      (s *ℤ (inr (inr x))) +ℤ ((neg-ℤ t) *ℤ (neg-ℤ (inr (inr y))))
-      ＝ (s *ℤ (inr (inr x))) +ℤ (t *ℤ (inr (inr y)))
-        by ap ((s *ℤ (inr (inr x))) +ℤ_)
-          (double-negative-law-mul-ℤ t (inr (inr y)))
-      ＝ gcd-ℤ (inr (inr x)) (inr (inr y))
-        by pr2 (pr2 (pos-bezout))
-      ＝ gcd-ℤ (inr (inr x)) (inl y)
-        by ap (λ M → (int-ℕ (gcd-ℕ (succ-ℕ x) M))) (abs-neg-ℤ (inr (inr y)))
+    ( ap
+      ( (s *ℤ (inr (inr x))) +ℤ_)
+      ( double-negative-law-mul-ℤ t (inr (inr y)))) ∙
+    ( pr2 (pr2 (pos-bezout))) ∙
+    ( ap (λ M → (int-ℕ (gcd-ℕ (succ-ℕ x) M))) (abs-neg-ℤ (inr (inr y))))
 bezouts-lemma-ℤ (inr (inr x)) (inr (inl star)) = pair one-ℤ (pair one-ℤ eqn)
   where
   eqn :
     (one-ℤ *ℤ (inr (inr x))) +ℤ (one-ℤ *ℤ (inr (inl star))) ＝
     gcd-ℤ (inr (inr x)) (inr (inl star))
   eqn =
-    equational-reasoning
-      (one-ℤ *ℤ (inr (inr x))) +ℤ (one-ℤ *ℤ (inr (inl star)))
-      ＝ (inr (inr x)) +ℤ (one-ℤ *ℤ (inr (inl star)))
-        by
-          ap
-            ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
-            ( left-unit-law-mul-ℤ (inr (inr x)))
-      ＝ (inr (inr x)) +ℤ zero-ℤ
-        by ap ((inr (inr x)) +ℤ_) (right-zero-law-mul-ℤ one-ℤ)
-      ＝ int-ℕ (abs-ℤ (inr (inr x)))
-        by right-unit-law-add-ℤ (inr (inr x))
-      ＝ gcd-ℤ (inr (inr x)) zero-ℤ
-        by
-          inv
-            ( is-id-is-gcd-zero-ℤ'
-              { inr (inr x)}
-              { gcd-ℤ (inr (inr x)) zero-ℤ}
-              ( refl))
+    ( ap
+      ( _+ℤ (one-ℤ *ℤ (inr (inl star))))
+      ( left-unit-law-mul-ℤ (inr (inr x)))) ∙
+    ( ap ((inr (inr x)) +ℤ_) (right-zero-law-mul-ℤ one-ℤ)) ∙
+    ( right-unit-law-add-ℤ (inr (inr x))) ∙
+    ( inv
+      ( is-id-is-gcd-zero-ℤ'
+        { inr (inr x)}
+        { gcd-ℤ (inr (inr x)) zero-ℤ}
+        ( refl)))
 bezouts-lemma-ℤ (inr (inr x)) (inr (inr y)) =
   bezouts-lemma-pos-ints (inr (inr x)) (inr (inr y)) star star
 ```
@@ -485,36 +360,20 @@ div-right-factor-coprime-ℤ x y z H K = pair ((s *ℤ z) +ℤ (t *ℤ k)) eqn
   div-yz = pr2 H
   eqn : ((s *ℤ z) +ℤ (t *ℤ k)) *ℤ x ＝ z
   eqn =
-    equational-reasoning
-      ((s *ℤ z) +ℤ (t *ℤ k)) *ℤ x
-      ＝ ((s *ℤ z) *ℤ x) +ℤ ((t *ℤ k) *ℤ x)
-        by right-distributive-mul-add-ℤ (s *ℤ z) (t *ℤ k) x
-      ＝ ((s *ℤ x) *ℤ z) +ℤ ((t *ℤ k) *ℤ x)
-        by ap (_+ℤ ((t *ℤ k) *ℤ x))
-        ( equational-reasoning
-            (s *ℤ z) *ℤ x
-            ＝ s *ℤ (z *ℤ x)
-              by associative-mul-ℤ s z x
-            ＝ s *ℤ (x *ℤ z)
-              by ap (s *ℤ_) (commutative-mul-ℤ z x)
-            ＝ (s *ℤ x) *ℤ z
-              by inv (associative-mul-ℤ s x z))
-      ＝ ((s *ℤ x) *ℤ z) +ℤ ((t *ℤ y) *ℤ z)
-        by ap (((s *ℤ x) *ℤ z) +ℤ_)
-    ( equational-reasoning
-        (t *ℤ k) *ℤ x
-        ＝ t *ℤ (k *ℤ x)
-          by associative-mul-ℤ t k x
-        ＝ t *ℤ (y *ℤ z)
-          by ap (t *ℤ_) div-yz
-        ＝ (t *ℤ y) *ℤ z
-          by inv (associative-mul-ℤ t y z))
-    ＝ ((s *ℤ x) +ℤ (t *ℤ y)) *ℤ z
-      by inv (right-distributive-mul-add-ℤ (s *ℤ x) (t *ℤ y) z)
-    ＝ one-ℤ *ℤ z
-      by ap (_*ℤ z) (bezout-eqn ∙ K)
-    ＝ z
-      by left-unit-law-mul-ℤ z
+    ( right-distributive-mul-add-ℤ (s *ℤ z) (t *ℤ k) x) ∙
+    ( ap
+        ( _+ℤ ((t *ℤ k) *ℤ x))
+        ( ( associative-mul-ℤ s z x) ∙
+          ( ap (s *ℤ_) (commutative-mul-ℤ z x)) ∙
+          ( inv (associative-mul-ℤ s x z)))) ∙
+    ( ap
+      ( ((s *ℤ x) *ℤ z) +ℤ_)
+      ( associative-mul-ℤ t k x ∙
+        ap (t *ℤ_) div-yz ∙
+        inv (associative-mul-ℤ t y z))) ∙
+    ( inv (right-distributive-mul-add-ℤ (s *ℤ x) (t *ℤ y) z)) ∙
+    ( ap (_*ℤ z) (bezout-eqn ∙ K)) ∙
+    ( left-unit-law-mul-ℤ z)
 
 div-right-factor-coprime-ℕ :
   (x y z : ℕ) → (div-ℕ x (y *ℕ z)) → (gcd-ℕ x y ＝ 1) → div-ℕ x z
@@ -524,6 +383,6 @@ div-right-factor-coprime-ℕ x y z H K =
       ( int-ℕ x)
       ( int-ℕ y)
       ( int-ℕ z)
-        ( tr (div-ℤ (int-ℕ x)) (inv (mul-int-ℕ y z)) (div-int-div-ℕ H))
+      ( tr (div-ℤ (int-ℕ x)) (inv (mul-int-ℕ y z)) (div-int-div-ℕ H))
       ( eq-gcd-gcd-int-ℕ x y ∙ ap int-ℕ K))
 ```
diff --git a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
index a1ea80e7c2..bc91aab126 100755
--- a/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/bezouts-lemma-natural-numbers.lagda.md
@@ -106,16 +106,10 @@ int-is-distance-between-multiples-ℕ :
   ( (int-ℕ (is-distance-between-multiples-fst-coeff-ℕ d)) *ℤ (int-ℕ x)) ＝
   ( int-ℕ (is-distance-between-multiples-snd-coeff-ℕ d)) *ℤ (int-ℕ y)
 int-is-distance-between-multiples-ℕ x y z (k , l , p) H =
-  equational-reasoning
-    (int-ℕ z) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
-    ＝ (int-ℕ z) +ℤ (int-ℕ (k *ℕ x))
-      by ap ((int-ℕ z) +ℤ_) (mul-int-ℕ k x)
-    ＝ int-ℕ (z +ℕ (k *ℕ x))
-      by add-int-ℕ z (k *ℕ x)
-    ＝ int-ℕ (l *ℕ y)
-      by ap (int-ℕ) (rewrite-left-dist-add-ℕ z (k *ℕ x) (l *ℕ y) H (inv p))
-    ＝ (int-ℕ l) *ℤ (int-ℕ y)
-      by inv (mul-int-ℕ l y)
+  ( ap ((int-ℕ z) +ℤ_) (mul-int-ℕ k x)) ∙
+  ( add-int-ℕ z (k *ℕ x)) ∙
+  ( ap (int-ℕ) (rewrite-left-dist-add-ℕ z (k *ℕ x) (l *ℕ y) H (inv p))) ∙
+  ( inv (mul-int-ℕ l y))
 
 div-mod-is-distance-between-multiples-ℕ :
   (x y z : ℕ) →
@@ -124,154 +118,87 @@ div-mod-is-distance-between-multiples-ℕ x y z (k , l , p) =
   kxly-case-split (linear-leq-ℕ (k *ℕ x) (l *ℕ y))
   where
   kxly-case-split :
-    leq-ℕ (k *ℕ x) (l *ℕ y) + leq-ℕ (l *ℕ y) (k *ℕ x) →
+    (k *ℕ x) ≤-ℕ (l *ℕ y) + (l *ℕ y) ≤-ℕ (k *ℕ x) →
     div-ℤ-Mod x (mod-ℕ x y) (mod-ℕ x z)
   kxly-case-split (inl kxly) =
     ( mod-ℕ x l ,
-      ( equational-reasoning
-        mul-ℤ-Mod x (mod-ℕ x l) (mod-ℕ x y)
-        ＝ mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) (mod-ℕ x y)
-          by inv (ap (λ p → mul-ℤ-Mod x p (mod-ℕ x y)) (mod-int-ℕ x l))
-        ＝ mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) (mod-ℤ x (int-ℕ y))
-          by inv (ap (λ p → mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) p) (mod-int-ℕ x y))
-        ＝ mod-ℤ x ((int-ℕ l) *ℤ (int-ℕ y))
-          by inv (preserves-mul-mod-ℤ x (int-ℕ l) (int-ℕ y))
-        ＝ mod-ℤ x ((int-ℕ z) +ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
-          by
-          inv
-            ( ap
-              ( mod-ℤ x)
-              ( int-is-distance-between-multiples-ℕ x y z (k , l , p) kxly))
-        ＝ add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x ((int-ℕ k) *ℤ (int-ℕ x)))
-          by preserves-add-mod-ℤ x (int-ℕ z) ((int-ℕ k) *ℤ (int-ℕ x))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x (int-ℕ z))
-            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x (int-ℕ x)))
-          by
-          ap
-            ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
-            ( preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x (int-ℕ z))
-            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x zero-ℤ))
-          by
-          ap
-            ( λ p →
-              add-ℤ-Mod x
-                ( mod-ℤ x (int-ℕ z))
-                ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
-            ( mod-int-ℕ x x ∙ (mod-refl-ℕ x ∙ inv (mod-zero-ℤ x)))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x (int-ℕ z))
-            ( mod-ℤ x ((int-ℕ k) *ℤ zero-ℤ))
-          by
-          ap
-            ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
-            ( inv (preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ))
-        ＝ add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x zero-ℤ)
-          by
-          ap
-            ( λ p → add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x p))
-            ( right-zero-law-mul-ℤ (int-ℕ k))
-        ＝ mod-ℤ x ((int-ℕ z) +ℤ zero-ℤ)
-          by inv (preserves-add-mod-ℤ x (int-ℕ z) zero-ℤ)
-        ＝ mod-ℤ x (int-ℕ z)
-          by ap (mod-ℤ x) (right-unit-law-add-ℤ (int-ℕ z))
-        ＝ mod-ℕ x z by mod-int-ℕ x z))
+      ( ( inv (ap (λ p → mul-ℤ-Mod x p (mod-ℕ x y)) (mod-int-ℕ x l))) ∙
+        ( inv (ap (λ p → mul-ℤ-Mod x (mod-ℤ x (int-ℕ l)) p) (mod-int-ℕ x y))) ∙
+        ( inv (preserves-mul-mod-ℤ x (int-ℕ l) (int-ℕ y))) ∙
+        ( inv
+          ( ap
+            ( mod-ℤ x)
+            ( int-is-distance-between-multiples-ℕ x y z (k , l , p) kxly))) ∙
+        ( preserves-add-mod-ℤ x (int-ℕ z) ((int-ℕ k) *ℤ (int-ℕ x))) ∙
+        ( ap
+          ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
+          ( preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x))) ∙
+        ( ap
+          ( λ p →
+            add-ℤ-Mod x
+              ( mod-ℤ x (int-ℕ z))
+              ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
+          ( mod-int-ℕ x x ∙ (mod-refl-ℕ x ∙ inv (mod-zero-ℤ x)))) ∙
+        ( ap
+          ( add-ℤ-Mod x (mod-ℤ x (int-ℕ z)))
+          ( inv (preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ))) ∙
+        ( ap
+          ( λ p → add-ℤ-Mod x (mod-ℤ x (int-ℕ z)) (mod-ℤ x p))
+          ( right-zero-law-mul-ℤ (int-ℕ k))) ∙
+        ( inv (preserves-add-mod-ℤ x (int-ℕ z) zero-ℤ)) ∙
+        ( ap (mod-ℤ x) (right-unit-law-add-ℤ (int-ℕ z))) ∙
+        ( mod-int-ℕ x z)))
   kxly-case-split (inr lykx) =
     ( mod-ℤ x (neg-ℤ (int-ℕ l)) ,
-      ( equational-reasoning
-        mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))) (mod-ℕ x y)
-        ＝ mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))) (mod-ℤ x (int-ℕ y))
-          by
-          inv
+      ( ( inv
+          ( ap
+            ( mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))))
+            ( mod-int-ℕ x y))) ∙
+        ( inv (preserves-mul-mod-ℤ x (neg-ℤ (int-ℕ l)) (int-ℕ y))) ∙
+        ( ap
+          ( mod-ℤ x)
+          ( inv (right-unit-law-add-ℤ ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))) ∙
+        ( preserves-add-mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) (zero-ℤ)) ∙
+        ( ap
+          ( λ p →
+            add-ℤ-Mod x
+              ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
+              ( mod-ℤ x p))
+          ( inv (right-zero-law-mul-ℤ (int-ℕ k)))) ∙
+        ( ap
+          ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
+          ( preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ)) ∙
+        ( ap
+          ( λ p →
+            add-ℤ-Mod x
+              ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
+              ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
+          ( mod-zero-ℤ x ∙ (inv (mod-refl-ℕ x) ∙ inv (mod-int-ℕ x x)))) ∙
+        ( ap
+          ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
+          ( inv (preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x)))) ∙
+        ( inv
+          ( preserves-add-mod-ℤ x
+            ( (neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))
+            ( (int-ℕ k) *ℤ (int-ℕ x)))) ∙
+        ( ap
+          ( mod-ℤ x)
+          ( ( ap
+              ( _+ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
+              ( left-negative-law-mul-ℤ (int-ℕ l) (int-ℕ y))) ∙
+            ( commutative-add-ℤ
+              ( neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
+              ( (int-ℕ k) *ℤ (int-ℕ x))) ∙
             ( ap
-              ( mul-ℤ-Mod x (mod-ℤ x (neg-ℤ (int-ℕ l))))
-              ( mod-int-ℕ x y))
-        ＝ mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))
-          by inv (preserves-mul-mod-ℤ x (neg-ℤ (int-ℕ l)) (int-ℕ y))
-        ＝ mod-ℤ x (((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ zero-ℤ)
-          by
-          ap
-            ( mod-ℤ x)
-            ( inv (right-unit-law-add-ℤ ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-            ( mod-ℤ x zero-ℤ)
-          by preserves-add-mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) (zero-ℤ)
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-            ( mod-ℤ x ((int-ℕ k) *ℤ zero-ℤ))
-          by
-          ap
-            ( λ p →
-              add-ℤ-Mod x
-                ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-                ( mod-ℤ x p))
-            ( inv (right-zero-law-mul-ℤ (int-ℕ k)))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x zero-ℤ))
-          by
-          ap
-            ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
-            ( preserves-mul-mod-ℤ x (int-ℕ k) zero-ℤ)
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-            ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) (mod-ℤ x (int-ℕ x)))
-          by
-          ap
-            ( λ p →
-              add-ℤ-Mod x
-                ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-                ( mul-ℤ-Mod x (mod-ℤ x (int-ℕ k)) p))
-            ( mod-zero-ℤ x ∙ (inv (mod-refl-ℕ x) ∙ inv (mod-int-ℕ x x)))
-        ＝ add-ℤ-Mod x
-            ( mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)))
-            ( mod-ℤ x ((int-ℕ k) *ℤ (int-ℕ x)))
-          by
-          ap
-            ( add-ℤ-Mod x (mod-ℤ x ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))))
-            ( inv (preserves-mul-mod-ℤ x (int-ℕ k) (int-ℕ x)))
-        ＝ mod-ℤ x
-            ( ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
-          by
-          inv
-            ( preserves-add-mod-ℤ x
-              ( (neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y))
-              ( (int-ℕ k) *ℤ (int-ℕ x)))
-        ＝ mod-ℤ x (int-ℕ z)
-          by
-          ap
-            ( mod-ℤ x)
-            ( equational-reasoning
-              ((neg-ℤ (int-ℕ l)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
-              ＝ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y))) +ℤ ((int-ℕ k) *ℤ (int-ℕ x))
-                by
-                ap
-                  ( _+ℤ ((int-ℕ k) *ℤ (int-ℕ x)))
-                  ( left-negative-law-mul-ℤ (int-ℕ l) (int-ℕ y))
-              ＝ ((int-ℕ k) *ℤ (int-ℕ x)) +ℤ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
-                by
-                commutative-add-ℤ
-                  ( neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
-                  ( (int-ℕ k) *ℤ (int-ℕ x))
-              ＝ add-ℤ
-                  ( (int-ℕ z) +ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
-                  ( neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y)))
-                by
-                ap
-                  ( _+ℤ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y))))
-                  ( inv
-                    ( int-is-distance-between-multiples-ℕ y x z
-                      ( is-distance-between-multiples-sym-ℕ x y z (k , l , p))
-                    ( lykx)))
-              ＝ int-ℕ z
-                by
-                is-retraction-right-add-neg-ℤ
-                  ( (int-ℕ l) *ℤ (int-ℕ y))
-                  ( int-ℕ z))
-              ＝ mod-ℕ x z by mod-int-ℕ x z))
+              ( _+ℤ (neg-ℤ ((int-ℕ l) *ℤ (int-ℕ y))))
+              ( inv
+                ( int-is-distance-between-multiples-ℕ y x z
+                  ( is-distance-between-multiples-sym-ℕ x y z (k , l , p))
+                ( lykx)))) ∙
+            ( is-retraction-right-add-neg-ℤ
+              ( (int-ℕ l) *ℤ (int-ℕ y))
+              ( int-ℕ z)))) ∙
+        ( mod-int-ℕ x z)))
 ```
 
 ### If `[y] | [z]` in `ℤ-Mod x`, then `z = dist-ℕ (kx, ly)` for some `k` and `l`
@@ -293,19 +220,13 @@ cong-div-mod-ℤ x y z (u , p) =
   cong-eq-mod-ℤ x
     ( (int-ℤ-Mod x u) *ℤ (int-ℕ y))
     ( int-ℕ z)
-    ( equational-reasoning
-      mod-ℤ x ((int-ℤ-Mod x u) *ℤ (int-ℕ y))
-      ＝ mul-ℤ-Mod x (mod-ℤ x (int-ℤ-Mod x u)) (mod-ℤ x (int-ℕ y))
-        by preserves-mul-mod-ℤ x (int-ℤ-Mod x u) (int-ℕ y)
-      ＝ mul-ℤ-Mod x u (mod-ℤ x (int-ℕ y))
-        by
-        ap
-          ( λ p → mul-ℤ-Mod x p (mod-ℤ x (int-ℕ y)))
-          ( is-section-int-ℤ-Mod x u)
-      ＝ mul-ℤ-Mod x u (mod-ℕ x y)
-        by ap (mul-ℤ-Mod x u) (mod-int-ℕ x y)
-      ＝ mod-ℕ x z by p
-      ＝ mod-ℤ x (int-ℕ z) by inv (mod-int-ℕ x z))
+    ( ( preserves-mul-mod-ℤ x (int-ℤ-Mod x u) (int-ℕ y)) ∙
+      ( ap
+        ( λ p → mul-ℤ-Mod x p (mod-ℤ x (int-ℕ y)))
+        ( is-section-int-ℤ-Mod x u)) ∙
+      ( ap (mul-ℤ-Mod x u) (mod-int-ℕ x y)) ∙
+      ( p) ∙
+      ( inv (mod-int-ℕ x z)))
 
 is-distance-between-multiples-div-mod-ℕ :
   (x y z : ℕ) →
@@ -351,71 +272,33 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
       ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x)))) ＝
     int-ℕ z
   a-eqn-pos =
-    equational-reasoning
-    add-ℤ
+    ( commutative-add-ℤ
       ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-      ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-    ＝ add-ℤ
-        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-      by
-      commutative-add-ℤ
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-    ＝ add-ℤ
-        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-      by
-      ap
-        ( _+ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-        ( inv (left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x))))
-    ＝ add-ℤ
+      ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))) ∙
+    ( ap
+      ( _+ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
+      ( inv (left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x))))) ∙
+    ( ap
+      ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
+      ( inv
+        ( is-section-right-add-neg-ℤ
+          ( int-ℕ z)
+          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))) ∙
+    ( inv
+      ( associative-add-ℤ
         ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-        ( add-ℤ
-          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))
-          ( int-ℕ z))
-      by
-      ap
-        ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
-        ( inv
-          ( is-section-right-add-neg-ℤ
-            ( int-ℕ z)
-            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z))))
-        ( int-ℕ z)
-      by
-      inv
-        ( associative-add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))
-          ( int-ℕ z))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( a *ℤ (int-ℕ (succ-ℕ x))))
-        ( int-ℕ z)
-      by
-      ap
-        ( λ p → (((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p) +ℤ (int-ℕ z))
-        ( inv (pr2 (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-          ( a *ℤ (int-ℕ (succ-ℕ x))))
-        ( int-ℕ z)
-      by
-      ap
-        ( λ p → (p +ℤ (a *ℤ (int-ℕ (succ-ℕ x)))) +ℤ (int-ℕ z))
-        ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x)))
-    ＝ zero-ℤ +ℤ (int-ℕ z)
-      by
-      ap
-        ( _+ℤ (int-ℕ z))
-        ( left-inverse-law-add-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-    ＝ int-ℕ z by left-unit-law-add-ℤ (int-ℕ z)
+        ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))
+        ( int-ℕ z))) ∙
+    ( ap
+      ( λ p → (((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p) +ℤ (int-ℕ z))
+      ( inv (pr2 (cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))) ∙
+    ( ap
+      ( λ p → (p +ℤ (a *ℤ (int-ℕ (succ-ℕ x)))) +ℤ (int-ℕ z))
+      ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x)))) ∙
+    ( ap
+      ( _+ℤ (int-ℕ z))
+      ( left-inverse-law-add-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))) ∙
+    ( left-unit-law-add-ℤ (int-ℕ z))
 
   a-extra-eqn-neg :
     add-ℤ
@@ -426,212 +309,107 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
           ( int-ℕ y))) ＝
     ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ int-ℕ y) +ℤ (neg-ℤ (a *ℤ int-ℕ (succ-ℕ x)))
   a-extra-eqn-neg =
-    equational-reasoning
-    add-ℤ
-      ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-      ( neg-ℤ
-        ( mul-ℤ
+    ( ap
+      ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
+      ( inv
+        ( left-negative-law-mul-ℤ
           ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-          ( int-ℕ y)))
-    ＝ add-ℤ
-        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-        ( mul-ℤ
-          ( neg-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))))
-          ( int-ℕ y))
-      by
-      ap
-        ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
-        ( inv
-          ( left-negative-law-mul-ℤ
-            ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-            ( int-ℕ y)))
-    ＝ add-ℤ
-        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-        ( ((int-ℤ-Mod (succ-ℕ x) u) +ℤ (neg-ℤ (int-ℕ (succ-ℕ x)))) *ℤ (int-ℕ y))
-      by
-      ap
-        ( λ p →
-          add-ℤ
-            ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-            ( p *ℤ (int-ℕ y)))
-        ( equational-reasoning
-          neg-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-          ＝ neg-ℤ ((neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)) +ℤ (int-ℕ (succ-ℕ x)))
-            by
-            ap
-              ( neg-ℤ)
-              ( commutative-add-ℤ
-                ( int-ℕ (succ-ℕ x))
-                ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-          ＝ add-ℤ
-              ( neg-ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-              ( neg-ℤ (int-ℕ (succ-ℕ x)))
-            by
-            distributive-neg-add-ℤ
-              ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))
-              ( int-ℕ (succ-ℕ x))
-          ＝ (int-ℤ-Mod (succ-ℕ x) u) +ℤ (neg-ℤ (int-ℕ (succ-ℕ x)))
-            by
-            ap
-              ( _+ℤ (neg-ℤ (int-ℕ (succ-ℕ x))))
-              ( neg-neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-    ＝ add-ℤ
-        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-        ( add-ℤ
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          ( (neg-ℤ (int-ℕ (succ-ℕ x))) *ℤ (int-ℕ y)))
-      by
-      ap
-        ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
-        ( right-distributive-mul-add-ℤ
-          ( int-ℤ-Mod (succ-ℕ x) u)
-          ( neg-ℤ (int-ℕ (succ-ℕ x)))
-          ( int-ℕ y))
-    ＝ add-ℤ
-        ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-        ( add-ℤ
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
-      by
-      ap
-        ( λ p →
-          add-ℤ
-            ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-            ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ p))
-        ( left-negative-law-mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( (int-ℕ y) *ℤ (int-ℕ (succ-ℕ x))))
+          ( int-ℕ y)))) ∙
+    ( ap
+      ( λ p →
+        add-ℤ
+          ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
+          ( p *ℤ (int-ℕ y)))
+      ( ( ap
+          ( neg-ℤ)
+          ( commutative-add-ℤ
+            ( int-ℕ (succ-ℕ x))
+            ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) ∙
+        ( distributive-neg-add-ℤ
+          ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))
+          ( int-ℕ (succ-ℕ x))) ∙
+        ( ap
+          ( _+ℤ (neg-ℤ (int-ℕ (succ-ℕ x))))
+          ( neg-neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))))) ∙
+    ( ap
+      ( (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
+      ( right-distributive-mul-add-ℤ
+        ( int-ℤ-Mod (succ-ℕ x) u)
+        ( neg-ℤ (int-ℕ (succ-ℕ x)))
+        ( int-ℕ y))) ∙
+    ( ap
+      ( λ p →
+        add-ℤ
+          ( ((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
+          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ p))
+      ( left-negative-law-mul-ℤ (int-ℕ (succ-ℕ x)) (int-ℕ y))) ∙
+    ( ap
+      ( _+ℤ
         ( add-ℤ
           ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
-      by
-      ap
-        ( _+ℤ
+          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))))
+      ( right-distributive-mul-add-ℤ (neg-ℤ a) (int-ℕ y) (int-ℕ (succ-ℕ x)))) ∙
+    ( ap
+      ( λ p →
+        add-ℤ
+          ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p)
           ( add-ℤ
             ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
             ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))))
-        ( right-distributive-mul-add-ℤ (neg-ℤ a) (int-ℕ y) (int-ℕ (succ-ℕ x)))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
-        ( add-ℤ
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
-      by
-      ap
-        ( λ p →
-          add-ℤ
-            ( ((neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))) +ℤ p)
-            ( add-ℤ
-              ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-              ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))))
-        ( commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x)))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-        ( add-ℤ
-          ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))
-          ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))))
-      by
-      interchange-law-add-add-ℤ
-        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-        ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-        ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
-    ＝ add-ℤ
-        ( add-ℤ
-          ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-        ( zero-ℤ)
-      by
-      ap
-        ( add-ℤ
-          ( add-ℤ
-            ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))
-          ( right-inverse-law-add-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))
-    ＝ add-ℤ
-        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-      by
-      right-unit-law-add-ℤ
+      ( commutative-mul-ℤ (int-ℕ y) (int-ℕ (succ-ℕ x)))) ∙
+    ( interchange-law-add-add-ℤ
+      ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
+      ( (int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y))
+      ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
+      ( neg-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))) ∙
+    ( ap
+      ( add-ℤ
         ( add-ℤ
           ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-    ＝ add-ℤ
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-        ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-      by
-      commutative-add-ℤ
+          ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))))
+        ( right-inverse-law-add-ℤ ((int-ℕ (succ-ℕ x)) *ℤ (int-ℕ y)))) ∙
+    ( right-unit-law-add-ℤ
+      ( add-ℤ
         ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-    ＝ add-ℤ
-        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-        ( neg-ℤ (a *ℤ (int-ℕ (succ-ℕ x))))
-      by
-      ap
-        ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ_)
-        ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x)))
+        ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))) ∙
+    ( commutative-add-ℤ
+      ( (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x)))
+      ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) ∙
+    ( ap
+      ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ_)
+      ( left-negative-law-mul-ℤ a (int-ℕ (succ-ℕ x))))
 
   uy-z-case-split :
     ( ( is-nonnegative-ℤ
         ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))) +
       ( is-nonnegative-ℤ
         ( neg-ℤ
-          ( add-ℤ
-            ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-            ( neg-ℤ (int-ℕ z)))))) →
+          ( ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ (neg-ℤ (int-ℕ z)))))) →
     is-distance-between-multiples-ℕ (succ-ℕ x) y z
   uy-z-case-split (inl uy-z) =
     ( abs-ℤ a ,
       nat-Fin (succ-ℕ x) u ,
-      ( equational-reasoning
-        dist-ℕ ((abs-ℤ a) *ℕ (succ-ℕ x)) ((nat-Fin (succ-ℕ x) u) *ℕ y)
-        ＝ dist-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y) ((abs-ℤ a) *ℕ (succ-ℕ x))
-          by
-          symmetric-dist-ℕ
-            ( (abs-ℤ a) *ℕ (succ-ℕ x))
+      ( symmetric-dist-ℕ
+          ( (abs-ℤ a) *ℕ (succ-ℕ x))
+          ( (nat-Fin (succ-ℕ x) u) *ℕ y) ∙
+        ( inv
+          ( dist-int-ℕ
             ( (nat-Fin (succ-ℕ x) u) *ℕ y)
-        ＝ dist-ℤ
-            ( int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y))
-            ( int-ℕ ((abs-ℤ a) *ℕ (succ-ℕ x)))
-          by
-          inv
-            ( dist-int-ℕ
-              ( (nat-Fin (succ-ℕ x) u) *ℕ y)
-              ( (abs-ℤ a) *ℕ (succ-ℕ x)))
-        ＝ dist-ℤ
-            ( int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y))
-            ( (int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x)))
-          by
-          ap
-            ( dist-ℤ (int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y)))
-            ( inv (mul-int-ℕ (abs-ℤ a) (succ-ℕ x)))
-        ＝ dist-ℤ
-            ( (int-ℕ (nat-Fin (succ-ℕ x) u)) *ℤ (int-ℕ y))
-            ( (int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x)))
-          by
-          ap
-            ( λ p → dist-ℤ p ((int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x))))
-            ( inv (mul-int-ℕ (nat-Fin (succ-ℕ x) u) y))
-        ＝ dist-ℤ
-            ( (int-ℕ (nat-Fin (succ-ℕ x) u)) *ℤ (int-ℕ y))
-            ( a *ℤ (int-ℕ (succ-ℕ x)))
-          by
-          ap
-            ( λ p →
-              dist-ℤ
-                ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-                ( p *ℤ (int-ℕ (succ-ℕ x))))
-            ( int-abs-is-nonnegative-ℤ a a-is-nonnegative-ℤ)
-        ＝ abs-ℤ (int-ℕ z)
-          by ap (abs-ℤ) a-eqn-pos
-        ＝ z
-          by abs-int-ℕ z))
+            ( (abs-ℤ a) *ℕ (succ-ℕ x)))) ∙
+        ( ap
+          ( dist-ℤ (int-ℕ ((nat-Fin (succ-ℕ x) u) *ℕ y)))
+          ( inv (mul-int-ℕ (abs-ℤ a) (succ-ℕ x)))) ∙
+        ( ap
+          ( λ p → dist-ℤ p ((int-ℕ (abs-ℤ a)) *ℤ (int-ℕ (succ-ℕ x))))
+          ( inv (mul-int-ℕ (nat-Fin (succ-ℕ x) u) y))) ∙
+        ( ap
+          ( λ p →
+            dist-ℤ
+              ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
+              ( p *ℤ (int-ℕ (succ-ℕ x))))
+          ( int-abs-is-nonnegative-ℤ a a-is-nonnegative-ℤ)) ∙
+        ( ap (abs-ℤ) a-eqn-pos) ∙
+        ( abs-int-ℕ z)))
     where
     a-is-nonnegative-ℤ : is-nonnegative-ℤ a
     a-is-nonnegative-ℤ =
@@ -644,101 +422,87 @@ is-distance-between-multiples-div-mod-ℕ (succ-ℕ x) y z (u , p) =
         ( is-nonnegative-int-ℕ (succ-ℕ x))
 
   uy-z-case-split (inr z-uy) =
-    ( (abs-ℤ a) +ℕ y ,
-      abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) ,
-      ( equational-reasoning
-        dist-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x))
-          (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)
-        ＝ dist-ℤ (int-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x)))
-          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
-        by inv (dist-int-ℕ (((abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x))
-          (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
-        ＝ dist-ℤ ((int-ℕ ((abs-ℤ a) +ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
-        by ap (λ p → dist-ℤ p (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)))
-          (inv (mul-int-ℕ ((abs-ℤ a) +ℕ y) (succ-ℕ x)))
-        ＝ dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
-        by
-          ap
-            ( λ p →
-              dist-ℤ
-                ( p *ℤ (int-ℕ (succ-ℕ x)))
-                ( int-ℕ (mul-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-                  (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y)))
-          (inv (add-int-ℕ (abs-ℤ a) y))
-        ＝ dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (mul-ℤ (int-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-          (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))))) (int-ℕ y))
-        by
-          ap
+    ( ( (abs-ℤ a) +ℕ y) ,
+      ( abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) ,
+      ( ( inv
+          ( dist-int-ℕ
+            ( ( ( abs-ℤ a) +ℕ y) *ℕ (succ-ℕ x))
+            ( ( abs-ℤ
+                ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) *ℕ
+              ( y)))) ∙
+        ( ap
+          ( λ p →
+            dist-ℤ
+              ( p)
+              ( int-ℕ
+                ( ( abs-ℤ
+                    ( ( int-ℕ (succ-ℕ x)) +ℤ
+                      ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) *ℕ
+                  ( y))))
+          ( inv (mul-int-ℕ ((abs-ℤ a) +ℕ y) (succ-ℕ x)))) ∙
+        ( ap
+          ( λ p →
+            dist-ℤ
+              ( p *ℤ (int-ℕ (succ-ℕ x)))
+              ( int-ℕ
+                ( ( abs-ℤ
+                    ( ( int-ℕ (succ-ℕ x)) +ℤ
+                      ( neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) *ℕ
+                  ( y))))
+          ( inv (add-int-ℕ (abs-ℤ a) y))) ∙
+        ( ap
             ( dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x))))
             ( inv (mul-int-ℕ (abs-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-              (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))
-        ＝ dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (mul-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-            (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℕ y))
-          by ap (λ p → dist-ℤ (((int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ
-              (int-ℕ (succ-ℕ x))) (p *ℤ (int-ℕ y)))
-          (int-abs-is-nonnegative-ℤ ((int-ℕ (succ-ℕ x)) +ℤ
-            (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℤ-Mod-bounded x u))
-        ＝ dist-ℤ
-            ( ((int-ℕ (abs-ℤ (neg-ℤ a))) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-            ( mul-ℤ
-              ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-              ( int-ℕ y))
-        by
-          ap
-            ( λ p →
-              dist-ℤ
-                ( ((int-ℕ p) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-                ( mul-ℤ
-                  ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
-                  ( int-ℕ y)))
-          (inv (abs-neg-ℤ a))
-        ＝ dist-ℤ (((neg-ℤ a) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (mul-ℤ
-            ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) (int-ℕ y))
-        by ap (λ p → dist-ℤ ((p +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
-          (((int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) *ℤ
-            (int-ℕ y)))
-          (int-abs-is-nonnegative-ℤ (neg-ℤ a) neg-a-is-nonnegative-ℤ)
-        ＝ abs-ℤ (int-ℕ z)
-        by ap abs-ℤ (a-extra-eqn-neg ∙ a-eqn-pos)
-        ＝ z by abs-int-ℕ z))
+              (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))) y))) ∙
+        ( ap
+          ( λ p →
+            dist-ℤ
+              ( ( (int-ℕ (abs-ℤ a)) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
+              ( p *ℤ (int-ℕ y)))
+          ( int-abs-is-nonnegative-ℤ
+            ( ( int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
+            ( int-ℤ-Mod-bounded x u))) ∙
+        ( ap
+          ( λ p →
+            dist-ℤ
+              ( ( ( int-ℕ p) +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
+              ( mul-ℤ
+                ( ( int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u)))
+                ( int-ℕ y)))
+          ( inv (abs-neg-ℤ a))) ∙
+      ( ap
+        ( λ p →
+          dist-ℤ
+            ( (p +ℤ (int-ℕ y)) *ℤ (int-ℕ (succ-ℕ x)))
+            ( ( (int-ℕ (succ-ℕ x)) +ℤ (neg-ℤ (int-ℤ-Mod (succ-ℕ x) u))) *ℤ
+              ( int-ℕ y)))
+        ( int-abs-is-nonnegative-ℤ (neg-ℤ a) neg-a-is-nonnegative-ℤ)) ∙
+      ( ap abs-ℤ (a-extra-eqn-neg ∙ a-eqn-pos)) ∙
+      ( abs-int-ℕ z)))
     where
     neg-a-is-nonnegative-ℤ : is-nonnegative-ℤ (neg-ℤ a)
-    neg-a-is-nonnegative-ℤ = (is-nonnegative-left-factor-mul-ℤ
-      (tr is-nonnegative-ℤ
-      (equational-reasoning
-        neg-ℤ (((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ (int-ℕ z)))
-        ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
-          (neg-ℤ (neg-ℤ (int-ℕ z)))
-        by (distributive-neg-add-ℤ
-          ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
-          (neg-ℤ (int-ℕ z)))
-        ＝ (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ
-          (int-ℕ z)
-        by ap ((neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_)
-          (neg-neg-ℤ (int-ℕ z))
-        ＝ add-ℤ (int-ℕ z)
-          (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-        by commutative-add-ℤ
-          (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
-          (int-ℕ z)
-        ＝ (neg-ℤ a) *ℤ (int-ℕ (succ-ℕ x))
-        by inv (pr2
-          (symmetric-cong-ℤ (int-ℕ (succ-ℕ x))
-            ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)) (int-ℕ z)
-            (cong-div-mod-ℤ (succ-ℕ x) y z (u , p)))))
-        z-uy) (is-nonnegative-int-ℕ (succ-ℕ x)))
+    neg-a-is-nonnegative-ℤ =
+      is-nonnegative-left-factor-mul-ℤ
+        ( tr
+          ( is-nonnegative-ℤ)
+          ( ( distributive-neg-add-ℤ
+              ( ( int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
+              ( neg-ℤ (int-ℕ z))) ∙
+            ( ap
+              ( ( neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))) +ℤ_)
+              ( neg-neg-ℤ (int-ℕ z))) ∙
+            ( commutative-add-ℤ
+              (neg-ℤ ((int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y)))
+              (int-ℕ z)) ∙
+            ( inv
+              ( pr2
+                ( symmetric-cong-ℤ
+                  ( int-ℕ (succ-ℕ x))
+                  ( (int-ℤ-Mod (succ-ℕ x) u) *ℤ (int-ℕ y))
+                  ( int-ℕ z)
+                  ( cong-div-mod-ℤ (succ-ℕ x) y z (u , p))))))
+          ( z-uy))
+        ( is-nonnegative-int-ℕ (succ-ℕ x))
 ```
 
 ### The type `is-distance-between-multiples-ℕ x y z` is decidable
@@ -769,7 +533,8 @@ distance `d` between multiples of `x` and `y`.
 
 ```agda
 pos-distance-between-multiples : (x y z : ℕ) → UU lzero
-pos-distance-between-multiples x y z = is-nonzero-ℕ (x +ℕ y) →
+pos-distance-between-multiples x y z =
+  is-nonzero-ℕ (x +ℕ y) →
   (is-nonzero-ℕ z) × (is-distance-between-multiples-ℕ x y z)
 
 is-inhabited-pos-distance-between-multiples :
@@ -785,13 +550,15 @@ is-inhabited-pos-distance-between-multiples (succ-ℕ x) y = pair (succ-ℕ x)
 
 minimal-pos-distance-between-multiples :
   (x y : ℕ) → minimal-element-ℕ (pos-distance-between-multiples x y)
-minimal-pos-distance-between-multiples x y = well-ordering-principle-ℕ
-  (pos-distance-between-multiples x y)
-  (λ z → is-decidable-function-type
-    (is-decidable-neg (is-decidable-is-zero-ℕ (x +ℕ y)))
-    (is-decidable-product (is-decidable-neg (is-decidable-is-zero-ℕ z))
-      (is-decidable-is-distance-between-multiples-ℕ x y z)))
-  (is-inhabited-pos-distance-between-multiples x y)
+minimal-pos-distance-between-multiples x y =
+  well-ordering-principle-ℕ
+    ( pos-distance-between-multiples x y)
+    ( λ z →
+      is-decidable-function-type
+        ( is-decidable-neg (is-decidable-is-zero-ℕ (x +ℕ y)))
+        ( is-decidable-product (is-decidable-neg (is-decidable-is-zero-ℕ z))
+          ( is-decidable-is-distance-between-multiples-ℕ x y z)))
+    ( is-inhabited-pos-distance-between-multiples x y)
 
 minimal-positive-distance : (x y : ℕ) → ℕ
 minimal-positive-distance x y = pr1 (minimal-pos-distance-between-multiples x y)
@@ -818,38 +585,40 @@ minimal-positive-distance-is-minimal x y =
 
 minimal-positive-distance-nonzero :
   (x y : ℕ) →
-  (is-nonzero-ℕ (x +ℕ y)) →
-  (is-nonzero-ℕ (minimal-positive-distance x y))
+  is-nonzero-ℕ (x +ℕ y) →
+  is-nonzero-ℕ (minimal-positive-distance x y)
 minimal-positive-distance-nonzero x y nonzero =
   pr1 ((pr1 (pr2 (minimal-pos-distance-between-multiples x y))) nonzero)
 
 minimal-positive-distance-leq-sym :
   (x y : ℕ) →
-  leq-ℕ (minimal-positive-distance x y) (minimal-positive-distance y x)
+  (minimal-positive-distance x y) ≤-ℕ (minimal-positive-distance y x)
 minimal-positive-distance-leq-sym x y =
-  minimal-positive-distance-is-minimal x y (minimal-positive-distance y x)
-  (λ H →
-    pair'
-      ( minimal-positive-distance-nonzero
-        ( y)
-        ( x)
-        ( λ K → H (commutative-add-ℕ x y ∙ K)))
-      ( is-distance-between-multiples-sym-ℕ
-        ( y)
-        ( x)
-        ( minimal-positive-distance y x)
-        ( minimal-positive-distance-is-distance
+  minimal-positive-distance-is-minimal x y
+    ( minimal-positive-distance y x)
+    ( λ H →
+      pair'
+        ( minimal-positive-distance-nonzero
           ( y)
           ( x)
-          ( λ K → H (commutative-add-ℕ x y ∙ K)))))
+          ( λ K → H (commutative-add-ℕ x y ∙ K)))
+        ( is-distance-between-multiples-sym-ℕ
+          ( y)
+          ( x)
+          ( minimal-positive-distance y x)
+          ( minimal-positive-distance-is-distance
+            ( y)
+            ( x)
+            ( λ K → H (commutative-add-ℕ x y ∙ K)))))
 
 minimal-positive-distance-sym :
   (x y : ℕ) → minimal-positive-distance x y ＝ minimal-positive-distance y x
-minimal-positive-distance-sym x y = antisymmetric-leq-ℕ
-  (minimal-positive-distance x y)
-  (minimal-positive-distance y x)
-  (minimal-positive-distance-leq-sym x y)
-  (minimal-positive-distance-leq-sym y x)
+minimal-positive-distance-sym x y =
+  antisymmetric-leq-ℕ
+    ( minimal-positive-distance x y)
+    ( minimal-positive-distance y x)
+    ( minimal-positive-distance-leq-sym x y)
+    ( minimal-positive-distance-leq-sym y x)
 
 minimal-positive-distance-x-coeff : (x y : ℕ) → (is-nonzero-ℕ (x +ℕ y)) → ℕ
 minimal-positive-distance-x-coeff x y H =
@@ -918,68 +687,31 @@ minimal-positive-distance-div-succ-x-eqn :
         ( succ-ℕ x))) ＝
       int-ℕ (succ-ℕ x)
 minimal-positive-distance-div-succ-x-eqn x y =
-    equational-reasoning
-      add-ℤ
-        ( mul-ℤ
-          ( int-ℕ
-            ( quotient-euclidean-division-ℕ
-              ( minimal-positive-distance (succ-ℕ x) y)
-              ( succ-ℕ x)))
-          ( int-ℕ (minimal-positive-distance (succ-ℕ x) y)))
-        ( int-ℕ
-          ( remainder-euclidean-division-ℕ
-            ( minimal-positive-distance (succ-ℕ x) y)
-            ( succ-ℕ x)))
-      ＝ add-ℤ
-          ( int-ℕ
-            ( mul-ℕ
-              ( quotient-euclidean-division-ℕ
-                ( minimal-positive-distance (succ-ℕ x) y)
-                ( succ-ℕ x))
-              ( minimal-positive-distance (succ-ℕ x) y)))
-          ( int-ℕ
-            ( remainder-euclidean-division-ℕ
-              ( minimal-positive-distance (succ-ℕ x) y)
-              ( succ-ℕ x)))
-          by
-            ( ap
-              ( _+ℤ
-                ( int-ℕ
-                  ( remainder-euclidean-division-ℕ
-                    ( minimal-positive-distance (succ-ℕ x) y)
-                    ( succ-ℕ x))))
-              ( mul-int-ℕ
-                ( quotient-euclidean-division-ℕ
-                  ( minimal-positive-distance (succ-ℕ x) y)
-                  ( succ-ℕ x))
-                ( minimal-positive-distance (succ-ℕ x) y)))
-      ＝ int-ℕ
-            ( add-ℕ
-              ( mul-ℕ
-                ( quotient-euclidean-division-ℕ
-                  ( minimal-positive-distance (succ-ℕ x) y)
-                  ( succ-ℕ x))
-                ( minimal-positive-distance (succ-ℕ x) y))
-              ( remainder-euclidean-division-ℕ
-                ( minimal-positive-distance (succ-ℕ x) y)
-                ( succ-ℕ x)))
-          by
-            ( add-int-ℕ
-              ( mul-ℕ
-                ( quotient-euclidean-division-ℕ
-                  ( minimal-positive-distance (succ-ℕ x) y)
-                  ( succ-ℕ x))
-                ( minimal-positive-distance (succ-ℕ x) y))
-              ( remainder-euclidean-division-ℕ
-                ( minimal-positive-distance (succ-ℕ x) y)
-                ( succ-ℕ x)))
-      ＝ int-ℕ (succ-ℕ x)
-          by
-            ap
-              ( int-ℕ)
-              ( eq-euclidean-division-ℕ
-                ( minimal-positive-distance (succ-ℕ x) y)
-                ( succ-ℕ x))
+  ( ap
+    ( _+ℤ
+      ( int-ℕ
+        ( remainder-euclidean-division-ℕ
+          ( minimal-positive-distance (succ-ℕ x) y)
+          ( succ-ℕ x))))
+    ( mul-int-ℕ
+      ( quotient-euclidean-division-ℕ
+        ( minimal-positive-distance (succ-ℕ x) y)
+        ( succ-ℕ x))
+      ( minimal-positive-distance (succ-ℕ x) y))) ∙
+  ( add-int-ℕ
+    ( mul-ℕ
+      ( quotient-euclidean-division-ℕ
+        ( minimal-positive-distance (succ-ℕ x) y)
+        ( succ-ℕ x))
+      ( minimal-positive-distance (succ-ℕ x) y))
+    ( remainder-euclidean-division-ℕ
+      ( minimal-positive-distance (succ-ℕ x) y)
+      ( succ-ℕ x))) ∙
+  ( ap
+    ( int-ℕ)
+    ( eq-euclidean-division-ℕ
+      ( minimal-positive-distance (succ-ℕ x) y)
+      ( succ-ℕ x)))
 
 remainder-min-dist-succ-x-le-min-dist :
   (x y : ℕ) →
@@ -1030,8 +762,8 @@ remainder-min-dist-succ-x-is-distance x y =
   dist-sx-ty-eq-d = minimal-positive-distance-succ-eqn x y
 
   sx-ty-case-split :
-    ( leq-ℕ (s *ℕ (succ-ℕ x)) (t *ℕ y) +
-      leq-ℕ (t *ℕ y) (s *ℕ (succ-ℕ x))) →
+    ( (s *ℕ (succ-ℕ x)) ≤-ℕ (t *ℕ y) +
+      (t *ℕ y) ≤-ℕ (s *ℕ (succ-ℕ x))) →
     is-distance-between-multiples-ℕ (succ-ℕ x) y r
   sx-ty-case-split (inl sxty) =
     ((q *ℕ s) +ℕ 1 , q *ℕ t , inv (dist-eqn))
@@ -1040,41 +772,24 @@ remainder-min-dist-succ-x-is-distance x y =
       int-ℕ d ＝
       ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
     add-dist-eqn =
-      equational-reasoning
-        int-ℕ d
-        ＝ ((int-ℕ d) +ℤ (int-ℕ (s *ℕ (succ-ℕ x)))) +ℤ
-          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-          by
-          inv
-            ( is-retraction-right-add-neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))) (int-ℕ d))
-        ＝ (int-ℕ (d +ℕ (s *ℕ (succ-ℕ x)))) +ℤ
-          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-          by
-          ap
-            ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
-            ( add-int-ℕ d (s *ℕ (succ-ℕ x)))
-        ＝ (int-ℕ (t *ℕ y)) +ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-          by ap (λ H → (int-ℕ H) +ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
-            (rewrite-left-dist-add-ℕ d (s *ℕ (succ-ℕ x))
-              (t *ℕ y) sxty (inv (dist-sx-ty-eq-d)))
-        ＝ ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-          by
-          ap
-            ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
-            ( inv (mul-int-ℕ t y))
-        ＝ ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))
-          by
-          ap
-            ( λ H → ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ (neg-ℤ H))
-            ( inv (mul-int-ℕ s (succ-ℕ x)))
-        ＝ ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-          ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
-          by
-          ap
-            ( ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ_)
-            ( inv (left-negative-law-mul-ℤ (int-ℕ s) (int-ℕ (succ-ℕ x))))
+      ( inv
+        ( is-retraction-right-add-neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x))) (int-ℕ d))) ∙
+      ( ap
+        ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
+        ( add-int-ℕ d (s *ℕ (succ-ℕ x)))) ∙
+      ( ap
+        ( λ H → (int-ℕ H) +ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
+        ( rewrite-left-dist-add-ℕ d
+          ( s *ℕ (succ-ℕ x)) (t *ℕ y) sxty (inv (dist-sx-ty-eq-d)))) ∙
+      ( ap
+        ( _+ℤ (neg-ℤ (int-ℕ (s *ℕ (succ-ℕ x)))))
+        ( inv (mul-int-ℕ t y))) ∙
+      ( ap
+        ( λ H → ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ (neg-ℤ H))
+        ( inv (mul-int-ℕ s (succ-ℕ x)))) ∙
+      ( ap
+        ( ((int-ℕ t) *ℤ (int-ℕ y)) +ℤ_)
+        ( inv (left-negative-law-mul-ℤ (int-ℕ s) (int-ℕ (succ-ℕ x)))))
 
     isolate-rem-eqn :
       int-ℕ r ＝
@@ -1087,50 +802,32 @@ remainder-min-dist-succ-x-is-distance x y =
               ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
         ( int-ℕ (succ-ℕ x))
     isolate-rem-eqn =
-      equational-reasoning
-        int-ℕ r
-        ＝ add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-          (add-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-              ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-          (int-ℕ r))
-          by inv (is-retraction-left-add-neg-ℤ
-            ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            (int-ℕ r))
-        ＝ add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-          (((int-ℕ q) *ℤ (int-ℕ d)) +ℤ (int-ℕ r))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( mul-ℤ
-                      ( int-ℕ q)
-                      ( add-ℤ
-                        ( (int-ℕ t) *ℤ (int-ℕ y))
-                        ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-                  ( ((int-ℕ q) *ℤ H) +ℤ (int-ℕ r)))
-              ( inv add-dist-eqn)
-        ＝ add-ℤ
+      ( inv
+        ( is-retraction-left-add-neg-ℤ
+          ( ( int-ℕ q) *ℤ
+            ( ( (int-ℕ t) *ℤ (int-ℕ y)) +ℤ
+              ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
+          ( int-ℕ r))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
             ( neg-ℤ
               ( mul-ℤ
                 ( int-ℕ q)
                 ( add-ℤ
                   ( (int-ℕ t) *ℤ (int-ℕ y))
                   ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
+            ( ( ( int-ℕ q) *ℤ H) +ℤ (int-ℕ r)))
+        ( inv add-dist-eqn)) ∙
+      ( ap
+        ( add-ℤ
+          ( neg-ℤ
+            ( mul-ℤ
+              ( int-ℕ q)
               ( add-ℤ
-                ( neg-ℤ
-                  ( mul-ℤ
-                    ( int-ℕ q)
-                    ( add-ℤ
-                      ( (int-ℕ t) *ℤ (int-ℕ y))
-                      ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))))
-              ( minimal-positive-distance-div-succ-x-eqn x y)
+                ( (int-ℕ t) *ℤ (int-ℕ y))
+                ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))))
+        ( minimal-positive-distance-div-succ-x-eqn x y))
 
     rearrange-arith-eqn :
       add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
@@ -1139,144 +836,94 @@ remainder-min-dist-succ-x-is-distance x y =
           (int-ℕ (succ-ℕ x)))
         (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
     rearrange-arith-eqn =
-      equational-reasoning
-        add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((int-ℕ t) *ℤ (int-ℕ y)) +ℤ
-          ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x))
-        ＝ add-ℤ (neg-ℤ (((int-ℕ q) *ℤ ((int-ℕ t) *ℤ (int-ℕ y))) +ℤ
-          ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            (int-ℕ (succ-ℕ x))
-          by (ap (λ H → (neg-ℤ H) +ℤ (int-ℕ (succ-ℕ x)))
-            (left-distributive-mul-add-ℤ (int-ℕ q) ((int-ℕ t) *ℤ (int-ℕ y))
-              ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-        ＝ add-ℤ (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            (int-ℕ (succ-ℕ x))
-          by (ap (λ H → add-ℤ (neg-ℤ (H +ℤ (mul-ℤ (int-ℕ q)
-            ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x)))
-              (inv (associative-mul-ℤ (int-ℕ q) (int-ℕ t) (int-ℕ y))))
-        ＝ add-ℤ (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            (int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ H))
-                  ( int-ℕ (succ-ℕ x)))
-            ( equational-reasoning
-                ((int-ℕ q) *ℤ ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))
-                ＝ ((int-ℕ q) *ℤ (neg-ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))
-                  by
-                    inv
-                      ( associative-mul-ℤ
-                        ( int-ℕ q)
-                        ( neg-ℤ (int-ℕ s))
-                        ( int-ℕ (succ-ℕ x)))
-                ＝ (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))
-                  by ap (_*ℤ (int-ℕ (succ-ℕ x)))
-                  (right-negative-law-mul-ℤ (int-ℕ q) (int-ℕ s))
-                ＝ neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
-                  by
-                    left-negative-law-mul-ℤ
-                      ( (int-ℕ q) *ℤ (int-ℕ s))
-                      ( int-ℕ (succ-ℕ x)))
-        ＝ add-ℤ
-            ( add-ℤ
-              ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-              ( neg-ℤ
-                ( neg-ℤ
-                  ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            (int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( _+ℤ (int-ℕ (succ-ℕ x)))
-              ( distributive-neg-add-ℤ
-                ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-        ＝ add-ℤ
-            ( add-ℤ
-              ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-              ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-              add-ℤ
-                ( (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))) +ℤ H)
-                ( int-ℕ (succ-ℕ x)))
-              ( neg-neg-ℤ
-                ( ((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))))
-        ＝ (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))) +ℤ
-          ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
-            (int-ℕ (succ-ℕ x)))
-          by associative-add-ℤ
-            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-            (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
-            (int-ℕ (succ-ℕ x))
-        ＝ add-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
-          (int-ℕ (succ-ℕ x)))
-          (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-          by commutative-add-ℤ
-            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-            ((((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
-            (int-ℕ (succ-ℕ x)))
-        ＝ add-ℤ
-            ( mul-ℤ
-              ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ one-ℤ)
-              ( int-ℕ (succ-ℕ x)))
-            ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-          by
-            ap
-              ( _+ℤ (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))))
-              ( ap
-                ( (((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
-                ( left-unit-law-mul-ℤ (int-ℕ (succ-ℕ x))) ∙
-                ( inv
-                  ( right-distributive-mul-add-ℤ
-                    ( (int-ℕ q) *ℤ (int-ℕ s))
-                    ( one-ℤ)
-                    ( int-ℕ (succ-ℕ x)))))
+      ( ap
+        ( λ H → (neg-ℤ H) +ℤ (int-ℕ (succ-ℕ x)))
+        ( left-distributive-mul-add-ℤ
+          ( int-ℕ q)
+          ( (int-ℕ t) *ℤ (int-ℕ y))
+          ( (neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
+            ( neg-ℤ
+              ( H +ℤ
+                ( mul-ℤ (int-ℕ q) ((neg-ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
+            ( int-ℕ (succ-ℕ x)))
+          ( inv (associative-mul-ℤ (int-ℕ q) (int-ℕ t) (int-ℕ y)))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
+            ( neg-ℤ
+              ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ H))
+            ( int-ℕ (succ-ℕ x)))
+        ( ( inv
+            ( associative-mul-ℤ
+              ( int-ℕ q)
+              ( neg-ℤ (int-ℕ s))
+              ( int-ℕ (succ-ℕ x)))) ∙
+          ( ap
+            ( _*ℤ (int-ℕ (succ-ℕ x)))
+            ( right-negative-law-mul-ℤ (int-ℕ q) (int-ℕ s))) ∙
+          ( left-negative-law-mul-ℤ
+            ( (int-ℕ q) *ℤ (int-ℕ s))
+            ( int-ℕ (succ-ℕ x))))) ∙
+      ( ap
+        ( _+ℤ (int-ℕ (succ-ℕ x)))
+        ( distributive-neg-add-ℤ
+          ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
+          ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
+            ( (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))) +ℤ H)
+            ( int-ℕ (succ-ℕ x)))
+        ( neg-neg-ℤ (((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))))) ∙
+      ( associative-add-ℤ
+          ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
+          ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))
+          ( int-ℕ (succ-ℕ x))) ∙
+      ( commutative-add-ℤ
+          ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
+          ( ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
+            ( int-ℕ (succ-ℕ x)))) ∙
+      ( ap
+        ( _+ℤ (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))))
+        ( ap
+          ( (((int-ℕ q) *ℤ ((int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))) +ℤ_)
+          ( left-unit-law-mul-ℤ (int-ℕ (succ-ℕ x))) ∙
+          ( inv
+            ( right-distributive-mul-add-ℤ
+              ( (int-ℕ q) *ℤ (int-ℕ s))
+              ( one-ℤ)
+              ( int-ℕ (succ-ℕ x))))))
 
     dist-eqn :
       r ＝ dist-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)) ((q *ℕ t) *ℕ y)
     dist-eqn =
-      equational-reasoning
-        r
-        ＝ abs-ℤ (int-ℕ r)
-          by (inv (abs-int-ℕ r))
-        ＝ dist-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ one-ℤ) *ℤ
-            (int-ℕ (succ-ℕ x)))
-          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-          by (ap (abs-ℤ) (isolate-rem-eqn ∙ rearrange-arith-eqn))
-        ＝ dist-ℤ
-            ( ((int-ℕ (q *ℕ s)) +ℤ (int-ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
-            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-          by ap (λ H → dist-ℤ ((H +ℤ (int-ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
-            (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-            (mul-int-ℕ q s)
-        ＝ dist-ℤ ((int-ℕ ((q *ℕ s) +ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
-          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-          by ap (λ H → dist-ℤ (H *ℤ (int-ℕ (succ-ℕ x)))
-            (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-            (add-int-ℕ (q *ℕ s) 1)
-        ＝ dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
-          (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-          by ap (λ H → dist-ℤ H (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-            (mul-int-ℕ ((q *ℕ s) +ℕ 1) (succ-ℕ x))
-        ＝ dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
-          ((int-ℕ (q *ℕ t)) *ℤ (int-ℕ y))
-          by ap (λ H → dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
-            (H *ℤ (int-ℕ y)))
-            (mul-int-ℕ q t)
-        ＝ dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)))
-          (int-ℕ ((q *ℕ t) *ℕ y))
-          by ap (dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))))
-            (mul-int-ℕ (q *ℕ t) y)
-        ＝ dist-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))
-          ((q *ℕ t) *ℕ y)
-          by dist-int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))
-            ((q *ℕ t) *ℕ y)
+      ( inv (abs-int-ℕ r)) ∙
+      ( ap (abs-ℤ) (isolate-rem-eqn ∙ rearrange-arith-eqn)) ∙
+      ( ap
+        ( λ H →
+          dist-ℤ
+            ( (H +ℤ (int-ℕ 1)) *ℤ (int-ℕ (succ-ℕ x)))
+            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
+        ( mul-int-ℕ q s)) ∙
+      ( ap
+        ( λ H →
+          dist-ℤ
+            ( H *ℤ (int-ℕ (succ-ℕ x)))
+            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
+        ( add-int-ℕ (q *ℕ s) 1)) ∙
+      ( ap
+        ( λ H → dist-ℤ H (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
+        ( mul-int-ℕ ((q *ℕ s) +ℕ 1) (succ-ℕ x))) ∙
+      ( ap
+        ( λ H → dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))) (H *ℤ (int-ℕ y)))
+        ( mul-int-ℕ q t)) ∙
+      ( ap
+        ( dist-ℤ (int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x))))
+        ( mul-int-ℕ (q *ℕ t) y)) ∙
+      ( dist-int-ℕ (((q *ℕ s) +ℕ 1) *ℕ (succ-ℕ x)) ((q *ℕ t) *ℕ y))
 
   sx-ty-case-split (inr tysx) =
     (abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) ,
@@ -1298,21 +945,15 @@ remainder-min-dist-succ-x-is-distance x y =
       where
       x-r-equality : succ-ℕ x ＝ r
       x-r-equality =
-        equational-reasoning
-          succ-ℕ x
-          ＝ (q *ℕ d) +ℕ r
-            by (inv (eq-euclidean-division-ℕ d (succ-ℕ x)))
-          ＝ (0 *ℕ d) +ℕ r
-            by (ap (λ H → (H *ℕ d) +ℕ r) iszero)
-          ＝ 0 +ℕ r
-            by (ap (_+ℕ r) (left-zero-law-mul-ℕ d))
-          ＝ r
-            by (left-unit-law-add-ℕ r)
-
-      le-x-d : le-ℕ (succ-ℕ x) d
+        (inv (eq-euclidean-division-ℕ d (succ-ℕ x))) ∙
+        (ap (λ H → (H *ℕ d) +ℕ r) iszero) ∙
+        (ap (_+ℕ r) (left-zero-law-mul-ℕ d)) ∙
+        (left-unit-law-add-ℕ r)
+
+      le-x-d : (succ-ℕ x) <-ℕ d
       le-x-d =
         tr
-          ( λ n → le-ℕ n d)
+          ( λ n → n <-ℕ d)
           ( inv (x-r-equality))
           ( remainder-min-dist-succ-x-le-min-dist x y)
 
@@ -1339,52 +980,43 @@ remainder-min-dist-succ-x-is-distance x y =
       where
       zero-addition : (t *ℕ y) +ℕ d ＝ 0
       zero-addition =
-        equational-reasoning
-          (t *ℕ y) +ℕ d
-          ＝ (s *ℕ (succ-ℕ x))
-            by rewrite-dist
-          ＝ (zero-ℕ *ℕ (succ-ℕ x))
-            by (ap (_*ℕ (succ-ℕ x)) iszero)
-          ＝ zero-ℕ
-            by (left-zero-law-mul-ℕ (succ-ℕ x))
+        ( rewrite-dist) ∙
+        ( ap (_*ℕ (succ-ℕ x)) iszero) ∙
+        ( left-zero-law-mul-ℕ (succ-ℕ x))
 
       d-is-zero : is-zero-ℕ d
       d-is-zero = is-zero-right-is-zero-add-ℕ (t *ℕ y) d (zero-addition)
 
     coeff-nonnegative : leq-ℤ one-ℤ ((int-ℕ q) *ℤ (int-ℕ s))
-    coeff-nonnegative = tr (leq-ℤ one-ℤ)
-      (inv (mul-int-ℕ q s)) (leq-int-ℕ 1 (q *ℕ s)
-        (leq-succ-le-ℕ 0 (q *ℕ s) (le-is-nonzero-ℕ (q *ℕ s)
-          (is-nonzero-mul-ℕ q s quotient-min-dist-succ-x-nonzero
-            min-dist-succ-x-coeff-nonzero))))
+    coeff-nonnegative =
+      tr
+        ( leq-ℤ one-ℤ)
+        ( inv (mul-int-ℕ q s))
+        ( leq-int-ℕ 1
+          ( q *ℕ s)
+          ( leq-succ-le-ℕ 0
+            ( q *ℕ s)
+            ( le-is-nonzero-ℕ (q *ℕ s)
+              ( is-nonzero-mul-ℕ q s
+                ( quotient-min-dist-succ-x-nonzero)
+                ( min-dist-succ-x-coeff-nonzero)))))
 
     add-dist-eqn :
       int-ℕ d ＝
       ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))
     add-dist-eqn =
-      equational-reasoning
-        int-ℕ d
-        ＝ (neg-ℤ (int-ℕ (t *ℕ y))) +ℤ ((int-ℕ (t *ℕ y)) +ℤ (int-ℕ d))
-          by inv (is-retraction-left-add-neg-ℤ (int-ℕ (t *ℕ y)) (int-ℕ d))
-        ＝ (neg-ℤ (int-ℕ (t *ℕ y))) +ℤ (int-ℕ ((t *ℕ y) +ℕ d))
-          by ap ((neg-ℤ (int-ℕ (t *ℕ y))) +ℤ_) (add-int-ℕ (t *ℕ y) d)
-        ＝ (neg-ℤ (int-ℕ (t *ℕ y))) +ℤ (int-ℕ (s *ℕ (succ-ℕ x)))
-          by ap (λ H → (neg-ℤ (int-ℕ (t *ℕ y))) +ℤ (int-ℕ H)) rewrite-dist
-        ＝ (neg-ℤ ((int-ℕ t) *ℤ (int-ℕ y))) +ℤ (int-ℕ (s *ℕ (succ-ℕ x)))
-          by
-            ap
-              ( λ H → (neg-ℤ H) +ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-              ( inv (mul-int-ℕ t y))
-        ＝ ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ (int-ℕ (s *ℕ (succ-ℕ x)))
-          by
-            ap
-              ( _+ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
-              ( inv (left-negative-law-mul-ℤ (int-ℕ t) (int-ℕ y)))
-        ＝ ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))
-          by
-            ap
-              ( ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
-              ( inv (mul-int-ℕ s (succ-ℕ x)))
+      ( inv (is-retraction-left-add-neg-ℤ (int-ℕ (t *ℕ y)) (int-ℕ d))) ∙
+      ( ap ((neg-ℤ (int-ℕ (t *ℕ y))) +ℤ_) (add-int-ℕ (t *ℕ y) d)) ∙
+      ( ap (λ H → (neg-ℤ (int-ℕ (t *ℕ y))) +ℤ (int-ℕ H)) rewrite-dist) ∙
+      ( ap
+        ( λ H → (neg-ℤ H) +ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
+        ( inv (mul-int-ℕ t y))) ∙
+      ( ap
+        ( _+ℤ (int-ℕ (s *ℕ (succ-ℕ x))))
+        ( inv (left-negative-law-mul-ℤ (int-ℕ t) (int-ℕ y)))) ∙
+      ( ap
+        ( ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
+        ( inv (mul-int-ℕ s (succ-ℕ x))))
 
     isolate-rem-eqn :
       int-ℕ r ＝
@@ -1397,231 +1029,142 @@ remainder-min-dist-succ-x-is-distance x y =
               ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
         ( int-ℕ (succ-ℕ x))
     isolate-rem-eqn =
-      equational-reasoning
-        int-ℕ r
-        ＝ add-ℤ
-            ( neg-ℤ
-              ( mul-ℤ
-                ( int-ℕ q)
-                ( add-ℤ
-                  ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                  ( ((int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( add-ℤ
-              ( mul-ℤ
-                ( int-ℕ q)
-                ( add-ℤ
-                  ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                  ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))
-              ( int-ℕ r))
-          by inv (is-retraction-left-add-neg-ℤ (mul-ℤ (int-ℕ q)
-            (((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-            ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))) (int-ℕ r))
-        ＝ add-ℤ
+      ( inv
+        ( is-retraction-left-add-neg-ℤ
+          ( mul-ℤ
+            ( int-ℕ q)
+            ( ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
+              ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))
+          ( int-ℕ r))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
             ( neg-ℤ
               ( mul-ℤ
                 ( int-ℕ q)
                 ( add-ℤ
                   ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
                   ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( ((int-ℕ q) *ℤ (int-ℕ d)) +ℤ (int-ℕ r))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( mul-ℤ
-                      ( int-ℕ q)
-                      ( add-ℤ
-                        ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                        ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-                  ( ((int-ℕ q) *ℤ H) +ℤ (int-ℕ r)))
-              ( inv add-dist-eqn)
-        ＝ add-ℤ
-            ( neg-ℤ
-              ( ( int-ℕ q) *ℤ
-                ( ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-                  ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
+            ( ((int-ℕ q) *ℤ H) +ℤ (int-ℕ r)))
+        ( inv add-dist-eqn)) ∙
+      ( ap
+        ( add-ℤ
+          ( neg-ℤ
+            ( mul-ℤ
+              ( int-ℕ q)
               ( add-ℤ
-                ( neg-ℤ
-                  ( mul-ℤ
-                    ( int-ℕ q)
-                    ( add-ℤ
-                      ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                      ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))))
-              ( minimal-positive-distance-div-succ-x-eqn x y)
+                ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
+                ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))))
+        ( minimal-positive-distance-div-succ-x-eqn x y))
 
     rearrange-arith :
-      add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-        ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x))
-      ＝ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-        (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
-          (int-ℕ (succ-ℕ x))))
+      ( neg-ℤ
+        ( (int-ℕ q) *ℤ
+          ( ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
+            ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))) +ℤ
+      ( int-ℕ (succ-ℕ x)) ＝
+      ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
+      ( neg-ℤ
+        ( (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ (int-ℕ (succ-ℕ x))))
     rearrange-arith =
-      equational-reasoning
-        add-ℤ (neg-ℤ ((int-ℕ q) *ℤ (((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x)))))) (int-ℕ (succ-ℕ x))
-        ＝ add-ℤ
-            ( neg-ℤ
-              ( add-ℤ
-                ( (int-ℕ q) *ℤ ((neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y)))
-                ( (int-ℕ q) *ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H → (neg-ℤ H) +ℤ (int-ℕ (succ-ℕ x)))
-              ( left-distributive-mul-add-ℤ
-                ( int-ℕ q)
-                ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))
-        ＝ add-ℤ
+      ( ap
+        ( λ H → (neg-ℤ H) +ℤ (int-ℕ (succ-ℕ x)))
+        ( left-distributive-mul-add-ℤ
+          ( int-ℕ q)
+          ( (neg-ℤ (int-ℕ t)) *ℤ (int-ℕ y))
+          ( (int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
             ( neg-ℤ
-              ( add-ℤ
-                ( ((int-ℕ q) *ℤ (neg-ℤ (int-ℕ t))) *ℤ (int-ℕ y))
-                ( (int-ℕ q) *ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( H +ℤ ((int-ℕ q) *ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
-                  ( int-ℕ (succ-ℕ x)))
-              ( inv (associative-mul-ℤ (int-ℕ q) (neg-ℤ (int-ℕ t)) (int-ℕ y)))
-        ＝ add-ℤ
+              ( H +ℤ ((int-ℕ q) *ℤ ((int-ℕ s) *ℤ (int-ℕ (succ-ℕ x))))))
+            ( int-ℕ (succ-ℕ x)))
+        ( inv (associative-mul-ℤ (int-ℕ q) (neg-ℤ (int-ℕ t)) (int-ℕ y)))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
             ( neg-ℤ
               ( add-ℤ
                 ( ((int-ℕ q) *ℤ (neg-ℤ (int-ℕ t))) *ℤ (int-ℕ y))
-                ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( add-ℤ
-                      ( ((int-ℕ q) *ℤ (neg-ℤ (int-ℕ t))) *ℤ (int-ℕ y))
-                      ( H)))
-                  ( int-ℕ (succ-ℕ x)))
-            ( inv (associative-mul-ℤ (int-ℕ q) (int-ℕ s) (int-ℕ (succ-ℕ x))))
-        ＝ add-ℤ
+                ( H)))
+            ( int-ℕ (succ-ℕ x)))
+        ( inv (associative-mul-ℤ (int-ℕ q) (int-ℕ s) (int-ℕ (succ-ℕ x))))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
             ( neg-ℤ
               ( add-ℤ
-                ( (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t))) *ℤ (int-ℕ y))
-                ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( neg-ℤ
-                    ( add-ℤ
-                      ( H *ℤ (int-ℕ y))
-                      ( mul-ℤ
-                        ( (int-ℕ q) *ℤ (int-ℕ s))
-                        ( int-ℕ (succ-ℕ x)))))
-                  ( int-ℕ (succ-ℕ x)))
-              ( right-negative-law-mul-ℤ (int-ℕ q) (int-ℕ t))
-        ＝ add-ℤ
-            ( add-ℤ
-              ( neg-ℤ ((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t))) *ℤ (int-ℕ y)))
-              ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            ( int-ℕ (succ-ℕ x))
-          by ap (_+ℤ (int-ℕ (succ-ℕ x)))
-            (distributive-neg-add-ℤ
-              ((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t))) *ℤ (int-ℕ y))
-              (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ
-              (int-ℕ (succ-ℕ x))))
-        ＝ add-ℤ
+                ( H *ℤ (int-ℕ y))
+                ( mul-ℤ
+                  ( (int-ℕ q) *ℤ (int-ℕ s))
+                  ( int-ℕ (succ-ℕ x)))))
+            ( int-ℕ (succ-ℕ x)))
+        ( right-negative-law-mul-ℤ (int-ℕ q) (int-ℕ t))) ∙
+      ( ap
+        ( _+ℤ (int-ℕ (succ-ℕ x)))
+        ( distributive-neg-add-ℤ
+          ( (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t))) *ℤ (int-ℕ y))
+          ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ
+            (int-ℕ (succ-ℕ x))))) ∙
+      ( ap
+          ( λ H →
+        add-ℤ
             ( add-ℤ
-              ( (neg-ℤ (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t)))) *ℤ (int-ℕ y))
+              ( H)
+              ( neg-ℤ
+                ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
+            ( int-ℕ (succ-ℕ x)))
+        ( inv
+          ( left-negative-law-mul-ℤ
+            ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t)))
+            ( int-ℕ y)))) ∙
+      ( ap
+        ( λ H →
+          (add-ℤ ((H *ℤ (int-ℕ y)) +ℤ
               ( neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            ( int-ℕ (succ-ℕ x))
-          by
-            ap
-            ( λ H →
-              add-ℤ
-                ( add-ℤ
-                  ( H)
-                  ( neg-ℤ
-                    ( ((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-                ( int-ℕ (succ-ℕ x)))
-            ( inv
-              ( left-negative-law-mul-ℤ
-                ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t)))
-                ( int-ℕ y)))
-        ＝ add-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
-            (int-ℕ (succ-ℕ x))
-          by ap (λ H → (add-ℤ ((H *ℤ (int-ℕ y)) +ℤ
-            (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) *ℤ (int-ℕ (succ-ℕ x)))))
               (int-ℕ (succ-ℕ x))))
-            (neg-neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t)))
-        ＝ add-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-            ((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))))
-          (int-ℕ (succ-ℕ x))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ H)
-                  ( int-ℕ (succ-ℕ x)))
-              ( inv
-                ( left-negative-law-mul-ℤ
-                  ( (int-ℕ q) *ℤ (int-ℕ s))
-                  ( int-ℕ (succ-ℕ x))))
-        ＝ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          (((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
-            (int-ℕ (succ-ℕ x)))
-          by associative-add-ℤ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-            ((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x)))
-            (int-ℕ (succ-ℕ x))
-        ＝ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          (((neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x))) +ℤ
-            ((neg-ℤ (neg-ℤ one-ℤ)) *ℤ (int-ℕ (succ-ℕ x))))
-          by
-            ap
-              ( λ H →
-                add-ℤ
-                  ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-                  ( add-ℤ
-                    ( mul-ℤ
-                      ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s)))
-                      ( int-ℕ (succ-ℕ x)))
-                    ( H *ℤ (int-ℕ (succ-ℕ x)))))
-              ( inv (neg-neg-ℤ one-ℤ))
-        ＝ add-ℤ
-            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-            ( mul-ℤ
+        ( neg-neg-ℤ ((int-ℕ q) *ℤ (int-ℕ t)))) ∙
+      ( ap
+        ( λ H →
+          add-ℤ
+            ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ H)
+            ( int-ℕ (succ-ℕ x)))
+        ( inv
+          ( left-negative-law-mul-ℤ
+            ( (int-ℕ q) *ℤ (int-ℕ s))
+            ( int-ℕ (succ-ℕ x))))) ∙
+      ( associative-add-ℤ
+        ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
+        ( (neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s))) *ℤ (int-ℕ (succ-ℕ x)))
+        ( int-ℕ (succ-ℕ x))) ∙
+      ( ap
+          ( λ H →
+            add-ℤ
+              ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
               ( add-ℤ
-                ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s)))
-                ( neg-ℤ (neg-ℤ one-ℤ)))
-              ( int-ℕ (succ-ℕ x)))
-          by
-            ap
-              ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
-              ( inv
-                ( right-distributive-mul-add-ℤ
+                ( mul-ℤ
                   ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s)))
-                  ( neg-ℤ (neg-ℤ one-ℤ))
-                  ( int-ℕ (succ-ℕ x))))
-        ＝ add-ℤ
-            ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y))
-            ( mul-ℤ (neg-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ
-            (neg-ℤ one-ℤ))) (int-ℕ (succ-ℕ x)))
-          by ap (λ H → ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-              (H *ℤ (int-ℕ (succ-ℕ x)))))
-              (inv (distributive-neg-add-ℤ
-                ((int-ℕ q) *ℤ (int-ℕ s)) (neg-ℤ one-ℤ)))
-        ＝ (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-          (neg-ℤ (mul-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ
-            (neg-ℤ one-ℤ)) (int-ℕ (succ-ℕ x))))
-          by ap ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
-            (left-negative-law-mul-ℤ
-              (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
-              (int-ℕ (succ-ℕ x)))
+                  ( int-ℕ (succ-ℕ x)))
+                ( H *ℤ (int-ℕ (succ-ℕ x)))))
+          ( inv (neg-neg-ℤ one-ℤ))) ∙
+        ( ap
+          ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
+          ( inv
+            ( right-distributive-mul-add-ℤ
+              ( neg-ℤ ((int-ℕ q) *ℤ (int-ℕ s)))
+              ( neg-ℤ (neg-ℤ one-ℤ))
+              ( int-ℕ (succ-ℕ x))))) ∙
+        ( ap
+          ( λ H →
+            ( ( ((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
+              ( H *ℤ (int-ℕ (succ-ℕ x)))))
+          ( inv
+            ( distributive-neg-add-ℤ ((int-ℕ q) *ℤ (int-ℕ s)) (neg-ℤ one-ℤ)))) ∙
+        ( ap
+          ( (((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ_)
+          ( left-negative-law-mul-ℤ
+            ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
+            ( int-ℕ (succ-ℕ x))))
 
     dist-eqn :
       r ＝
@@ -1631,74 +1174,44 @@ remainder-min-dist-succ-x-is-distance x y =
           ( succ-ℕ x))
         ( (q *ℕ t) *ℕ y)
     dist-eqn =
-      equational-reasoning
-        r
-        ＝ abs-ℤ (int-ℕ r) by (inv (abs-int-ℕ r))
-        ＝ abs-ℤ ((((int-ℕ q) *ℤ (int-ℕ t)) *ℤ (int-ℕ y)) +ℤ
-            (neg-ℤ ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
-            (int-ℕ (succ-ℕ x)))))
-          by (ap abs-ℤ (isolate-rem-eqn ∙ rearrange-arith))
-        ＝ dist-ℤ ((int-ℕ (q *ℕ t)) *ℤ (int-ℕ y))
-          ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
-            (int-ℕ (succ-ℕ x)))
-          by ap (λ H → (dist-ℤ (H *ℤ (int-ℕ y))
-            ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
-              (int-ℕ (succ-ℕ x)))))
-              (mul-int-ℕ q t)
-        ＝ dist-ℤ (int-ℕ ((q *ℕ t) *ℕ y))
-          ((((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
-          (int-ℕ (succ-ℕ x)))
-          by
-            ap
-              ( λ H →
-                dist-ℤ H
-                  ( mul-ℤ
-                    ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
-                    ( int-ℕ (succ-ℕ x))))
-              ( mul-int-ℕ (q *ℕ t) y)
-        ＝ dist-ℤ
-            ( int-ℕ ((q *ℕ t) *ℕ y))
+      ( inv (abs-int-ℕ r)) ∙
+      ( ap abs-ℤ (isolate-rem-eqn ∙ rearrange-arith)) ∙
+      ( ap
+        ( λ H →
+          ( dist-ℤ
+            ( H *ℤ (int-ℕ y))
+            ( ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)) *ℤ
+              ( int-ℕ (succ-ℕ x)))))
+        ( mul-int-ℕ q t)) ∙
+      ( ap
+        ( λ H →
+          dist-ℤ H
             ( mul-ℤ
-              ( int-ℕ (abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))))
-              ( int-ℕ (succ-ℕ x)))
-          by
-            ap
-              ( λ H →
-                dist-ℤ
-                  ( int-ℕ ((q *ℕ t) *ℕ y))
-                  ( H *ℤ (int-ℕ (succ-ℕ x))))
-              ( inv
-                ( int-abs-is-nonnegative-ℤ
-                  ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
-                  ( coeff-nonnegative)))
-        ＝ dist-ℤ
+              ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
+              ( int-ℕ (succ-ℕ x))))
+        ( mul-int-ℕ (q *ℕ t) y)) ∙
+      ( ap
+        ( λ H →
+          dist-ℤ
             ( int-ℕ ((q *ℕ t) *ℕ y))
-            ( int-ℕ
-              ( mul-ℕ
-                ( abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)))
-                ( succ-ℕ x)))
-          by
-            ap
-              ( dist-ℤ (int-ℕ ((q *ℕ t) *ℕ y)))
-              ( mul-int-ℕ
-                ( abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)))
-                ( succ-ℕ x))
-        ＝ dist-ℕ ((q *ℕ t) *ℕ y)
-          ((abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))) *ℕ
-            (succ-ℕ x))
-          by dist-int-ℕ
-            ((q *ℕ t) *ℕ y)
-            ((abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))) *ℕ
-              (succ-ℕ x))
-        ＝ dist-ℕ
-          ((abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))) *ℕ
-            (succ-ℕ x))
-            ((q *ℕ t) *ℕ y)
-          by symmetric-dist-ℕ
-            ((q *ℕ t) *ℕ y)
-            (mul-ℕ (abs-ℤ (add-ℤ (mul-ℤ (int-ℕ q)
-              (int-ℕ s)) (neg-ℤ one-ℤ)))
-            (succ-ℕ x))
+            ( H *ℤ (int-ℕ (succ-ℕ x))))
+        ( inv
+          ( int-abs-is-nonnegative-ℤ
+            ( ((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))
+            ( coeff-nonnegative)))) ∙
+      ( ap
+        ( dist-ℤ (int-ℕ ((q *ℕ t) *ℕ y)))
+        ( mul-int-ℕ
+          ( abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ)))
+          ( succ-ℕ x))) ∙
+      ( dist-int-ℕ
+            ( (q *ℕ t) *ℕ y)
+            ( ( abs-ℤ (((int-ℕ q) *ℤ (int-ℕ s)) +ℤ (neg-ℤ one-ℤ))) *ℕ
+              ( succ-ℕ x))) ∙
+      ( symmetric-dist-ℕ
+        ( (q *ℕ t) *ℕ y)
+        ( ( abs-ℤ (add-ℤ (mul-ℤ (int-ℕ q) (int-ℕ s)) (neg-ℤ one-ℤ))) *ℕ
+          ( succ-ℕ x)))
 
 remainder-min-dist-succ-x-not-is-nonzero :
   (x y : ℕ) →
@@ -1784,48 +1297,23 @@ minimal-positive-distance-div-fst (succ-ℕ x) y =
       ( minimal-positive-distance (succ-ℕ x) y)) ＝
     ( succ-ℕ x)
   eqn =
-    equational-reasoning
-      mul-ℕ
-        ( quotient-euclidean-division-ℕ
-          ( minimal-positive-distance (succ-ℕ x) y)
-          ( succ-ℕ x))
-        ( minimal-positive-distance (succ-ℕ x) y)
-      ＝ add-ℕ
-          ( mul-ℕ
-            ( quotient-euclidean-division-ℕ
-              ( minimal-positive-distance (succ-ℕ x) y)
-              ( succ-ℕ x))
-            ( minimal-positive-distance (succ-ℕ x) y))
-          ( zero-ℕ)
-        by
-          ( inv
-            ( right-unit-law-add-ℕ
-              ( ( quotient-euclidean-division-ℕ
-                  ( minimal-positive-distance (succ-ℕ x) y)
-                  ( succ-ℕ x)) *ℕ
-                ( minimal-positive-distance (succ-ℕ x) y))))
-      ＝ add-ℕ
+    ( inv
+      ( right-unit-law-add-ℕ
         ( ( quotient-euclidean-division-ℕ
             ( minimal-positive-distance (succ-ℕ x) y)
             ( succ-ℕ x)) *ℕ
-          ( minimal-positive-distance (succ-ℕ x) y))
-        ( remainder-euclidean-division-ℕ
-          ( minimal-positive-distance (succ-ℕ x) y)
-          ( succ-ℕ x))
-        by
-          ( ap
-            ( add-ℕ
-              ( mul-ℕ
-                ( quotient-euclidean-division-ℕ
-                  ( minimal-positive-distance (succ-ℕ x) y)
-                  ( succ-ℕ x))
-                ( minimal-positive-distance (succ-ℕ x) y)))
-            ( inv (remainder-min-dist-succ-x-is-zero x y)))
-      ＝ succ-ℕ x
-        by
-          eq-euclidean-division-ℕ
+          ( minimal-positive-distance (succ-ℕ x) y)))) ∙
+    ( ap
+      ( add-ℕ
+        ( mul-ℕ
+          ( quotient-euclidean-division-ℕ
             ( minimal-positive-distance (succ-ℕ x) y)
-            ( succ-ℕ x)
+            ( succ-ℕ x))
+          ( minimal-positive-distance (succ-ℕ x) y)))
+      ( inv (remainder-min-dist-succ-x-is-zero x y))) ∙
+    ( eq-euclidean-division-ℕ
+      ( minimal-positive-distance (succ-ℕ x) y)
+      ( succ-ℕ x))
 
 minimal-positive-distance-div-snd :
   (x y : ℕ) → div-ℕ (minimal-positive-distance x y) y
@@ -1878,12 +1366,12 @@ gcd-ℕ-div-dist-between-mult x y z dist =
   t = is-distance-between-multiples-snd-coeff-ℕ dist
 
   sx-ty-case-split :
-    (leq-ℕ (s *ℕ x) (t *ℕ y) + leq-ℕ (t *ℕ y) (s *ℕ x)) →
+    ((s *ℕ x) ≤-ℕ (t *ℕ y) + (t *ℕ y) ≤-ℕ (s *ℕ x)) →
     div-ℕ (gcd-ℕ x y) z
   sx-ty-case-split (inl sxty) =
     div-right-summand-ℕ (gcd-ℕ x y) (s *ℕ x) z
-      (gcd-ℕ-div-x-mults x y z dist)
-      (concatenate-div-eq-ℕ (gcd-ℕ-div-y-mults x y z dist)
+      ( gcd-ℕ-div-x-mults x y z dist)
+      ( concatenate-div-eq-ℕ (gcd-ℕ-div-y-mults x y z dist)
         (inv rewrite-dist))
     where
     rewrite-dist : (s *ℕ x) +ℕ z ＝ t *ℕ y
diff --git a/src/elementary-number-theory/binomial-coefficients.lagda.md b/src/elementary-number-theory/binomial-coefficients.lagda.md
index 47b9960243..ad2b0fc359 100644
--- a/src/elementary-number-theory/binomial-coefficients.lagda.md
+++ b/src/elementary-number-theory/binomial-coefficients.lagda.md
@@ -49,7 +49,7 @@ binomial-coefficient-Fin n x = binomial-coefficient-ℕ n (nat-Fin (succ-ℕ n)
 
 ```agda
 is-zero-binomial-coefficient-ℕ :
-  (n k : ℕ) → le-ℕ n k → is-zero-ℕ (binomial-coefficient-ℕ n k)
+  (n k : ℕ) → n <-ℕ k → is-zero-ℕ (binomial-coefficient-ℕ n k)
 is-zero-binomial-coefficient-ℕ zero-ℕ (succ-ℕ k) _ = refl
 is-zero-binomial-coefficient-ℕ (succ-ℕ n) (succ-ℕ k) H =
   ap-add-ℕ
diff --git a/src/elementary-number-theory/congruence-natural-numbers.lagda.md b/src/elementary-number-theory/congruence-natural-numbers.lagda.md
index 57781d53a3..cd547aa5b0 100644
--- a/src/elementary-number-theory/congruence-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/congruence-natural-numbers.lagda.md
@@ -61,7 +61,7 @@ is-indiscrete-cong-one-ℕ x y = div-one-ℕ (dist-ℕ x y)
 is-discrete-cong-zero-ℕ :
   (x y : ℕ) → cong-ℕ zero-ℕ x y → x ＝ y
 is-discrete-cong-zero-ℕ x y (pair k p) =
-  eq-dist-ℕ x y ((inv p) ∙ (right-zero-law-mul-ℕ k))
+  eq-dist-ℕ x y (inv p ∙ right-zero-law-mul-ℕ k)
 
 cong-zero-ℕ :
   (k : ℕ) → cong-ℕ k k zero-ℕ
@@ -114,14 +114,14 @@ concatenate-eq-cong-eq-cong-eq-ℕ k
 
 ```agda
 eq-cong-le-dist-ℕ :
-  (k x y : ℕ) → le-ℕ (dist-ℕ x y) k → cong-ℕ k x y → x ＝ y
+  (k x y : ℕ) → dist-ℕ x y <-ℕ k → cong-ℕ k x y → x ＝ y
 eq-cong-le-dist-ℕ k x y H K =
   eq-dist-ℕ x y (is-zero-div-ℕ k (dist-ℕ x y) H K)
 ```
 
 ```agda
 eq-cong-le-ℕ :
-  (k x y : ℕ) → le-ℕ x k → le-ℕ y k → cong-ℕ k x y → x ＝ y
+  (k x y : ℕ) → x <-ℕ k → y <-ℕ k → cong-ℕ k x y → x ＝ y
 eq-cong-le-ℕ k x y H K =
   eq-cong-le-dist-ℕ k x y (strict-upper-bound-dist-ℕ k x y H K)
 ```
diff --git a/src/elementary-number-theory/decidable-types.lagda.md b/src/elementary-number-theory/decidable-types.lagda.md
index 047ada9a91..889700c472 100644
--- a/src/elementary-number-theory/decidable-types.lagda.md
+++ b/src/elementary-number-theory/decidable-types.lagda.md
@@ -101,10 +101,10 @@ is-decidable-strictly-bounded-Σ-ℕ m P Q dP dQ H =
 
 is-decidable-strictly-bounded-Σ-ℕ' :
   {l : Level} (m : ℕ) (P : ℕ → UU l) (d : is-decidable-fam P) →
-  is-decidable (Σ ℕ (λ x → (le-ℕ x m) × (P x)))
+  is-decidable (Σ ℕ (λ x → (x <-ℕ m) × (P x)))
 is-decidable-strictly-bounded-Σ-ℕ' m P d =
   is-decidable-strictly-bounded-Σ-ℕ m
-    ( λ x → le-ℕ x m)
+    ( λ x → x <-ℕ m)
     ( P)
     ( λ x → is-decidable-le-ℕ x m)
     ( d)
@@ -171,10 +171,10 @@ is-decidable-strictly-bounded-Π-ℕ P Q dP dQ m H =
 
 is-decidable-strictly-bounded-Π-ℕ' :
   {l : Level} (P : ℕ → UU l) (d : is-decidable-fam P) (m : ℕ) →
-  is-decidable ((x : ℕ) → le-ℕ x m → P x)
+  is-decidable ((x : ℕ) → x <-ℕ m → P x)
 is-decidable-strictly-bounded-Π-ℕ' P d m =
   is-decidable-strictly-bounded-Π-ℕ
-    ( λ x → le-ℕ x m)
+    ( λ x → x <-ℕ m)
     ( P)
     ( λ x → is-decidable-le-ℕ x m)
     ( d)
diff --git a/src/elementary-number-theory/distance-natural-numbers.lagda.md b/src/elementary-number-theory/distance-natural-numbers.lagda.md
index 0426593e35..42ea1e9ae1 100644
--- a/src/elementary-number-theory/distance-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/distance-natural-numbers.lagda.md
@@ -281,7 +281,7 @@ leq-dist-ℕ (succ-ℕ x) (succ-ℕ y) H =
 
 ```agda
 strict-upper-bound-dist-ℕ :
-  (b x y : ℕ) → le-ℕ x b → le-ℕ y b → le-ℕ (dist-ℕ x y) b
+  (b x y : ℕ) → x <-ℕ b → y <-ℕ b → dist-ℕ x y <-ℕ b
 strict-upper-bound-dist-ℕ (succ-ℕ b) zero-ℕ y H K = K
 strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) zero-ℕ H K = H
 strict-upper-bound-dist-ℕ (succ-ℕ b) (succ-ℕ x) (succ-ℕ y) H K =
diff --git a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
index ba0b3c9131..69a95fcb2c 100644
--- a/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/divisibility-natural-numbers.lagda.md
@@ -162,12 +162,12 @@ leq-div-ℕ d x f H with is-successor-is-nonzero-ℕ f
 ... | (pair y refl) = leq-div-succ-ℕ d y H
 
 leq-quotient-div-ℕ :
-  (d x : ℕ) → is-nonzero-ℕ x → (H : div-ℕ d x) → leq-ℕ (quotient-div-ℕ d x H) x
+  (d x : ℕ) → is-nonzero-ℕ x → (H : div-ℕ d x) → quotient-div-ℕ d x H ≤-ℕ x
 leq-quotient-div-ℕ d x f H =
   leq-div-ℕ (quotient-div-ℕ d x H) x f (div-quotient-div-ℕ d x H)
 
 leq-quotient-div-ℕ' :
-  (d x : ℕ) → is-nonzero-ℕ d → (H : div-ℕ d x) → leq-ℕ (quotient-div-ℕ d x H) x
+  (d x : ℕ) → is-nonzero-ℕ d → (H : div-ℕ d x) → quotient-div-ℕ d x H ≤-ℕ x
 leq-quotient-div-ℕ' d zero-ℕ f (zero-ℕ , p) = star
 leq-quotient-div-ℕ' d zero-ℕ f (succ-ℕ n , p) =
   f (is-zero-right-is-zero-add-ℕ _ d p)
@@ -179,10 +179,10 @@ leq-quotient-div-ℕ' d (succ-ℕ x) f H =
 
 ```agda
 le-div-succ-ℕ :
-  (d x : ℕ) → div-ℕ d (succ-ℕ x) → d ≠ succ-ℕ x → le-ℕ d (succ-ℕ x)
+  (d x : ℕ) → div-ℕ d (succ-ℕ x) → d ≠ succ-ℕ x → d <-ℕ succ-ℕ x
 le-div-succ-ℕ d x H f = le-leq-neq-ℕ (leq-div-succ-ℕ d x H) f
 
-le-div-ℕ : (d x : ℕ) → is-nonzero-ℕ x → div-ℕ d x → d ≠ x → le-ℕ d x
+le-div-ℕ : (d x : ℕ) → is-nonzero-ℕ x → div-ℕ d x → d ≠ x → d <-ℕ x
 le-div-ℕ d x H K f = le-leq-neq-ℕ (leq-div-ℕ d x H K) f
 ```
 
@@ -250,7 +250,7 @@ leq-one-div-ℕ d x H L =
 
 ```agda
 is-zero-div-ℕ :
-  (d x : ℕ) → le-ℕ x d → div-ℕ d x → is-zero-ℕ x
+  (d x : ℕ) → x <-ℕ d → div-ℕ d x → is-zero-ℕ x
 is-zero-div-ℕ d zero-ℕ H D = refl
 is-zero-div-ℕ d (succ-ℕ x) H (pair (succ-ℕ k) p) =
   ex-falso
@@ -512,11 +512,11 @@ is-one-divisor-ℕ d x f (.x , q) refl =
 ```agda
 le-quotient-div-ℕ :
   (d x : ℕ) → is-nonzero-ℕ x → (H : div-ℕ d x) → ¬ (is-one-ℕ d) →
-  le-ℕ (quotient-div-ℕ d x H) x
+  (quotient-div-ℕ d x H) <-ℕ x
 le-quotient-div-ℕ d x f H g =
   map-left-unit-law-coproduct-is-empty
     ( quotient-div-ℕ d x H ＝ x)
-    ( le-ℕ (quotient-div-ℕ d x H) x)
+    ( quotient-div-ℕ d x H <-ℕ x)
     ( map-neg (is-one-divisor-ℕ d x f H) g)
     ( eq-or-le-leq-ℕ
       ( quotient-div-ℕ d x H)
diff --git a/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md b/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
index 1ef17f8247..92d447b645 100644
--- a/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/euclidean-division-natural-numbers.lagda.md
@@ -76,7 +76,7 @@ quotient-euclidean-division-ℕ' (succ-ℕ k) n =
 
 ```agda
 euclidean-division-ℕ :
-  (k x : ℕ) → Σ ℕ (λ r → (cong-ℕ k x r) × (is-nonzero-ℕ k → le-ℕ r k))
+  (k x : ℕ) → Σ ℕ (λ r → (cong-ℕ k x r) × (is-nonzero-ℕ k → r <-ℕ k))
 pr1 (euclidean-division-ℕ zero-ℕ x) = x
 pr1 (pr2 (euclidean-division-ℕ zero-ℕ x)) = refl-cong-ℕ zero-ℕ x
 pr2 (pr2 (euclidean-division-ℕ zero-ℕ x)) f = ex-falso (f refl)
@@ -100,7 +100,7 @@ cong-euclidean-division-ℕ k x =
   pr1 (pr2 (euclidean-division-ℕ k x))
 
 strict-upper-bound-remainder-euclidean-division-ℕ :
-  (k x : ℕ) → is-nonzero-ℕ k → le-ℕ (remainder-euclidean-division-ℕ k x) k
+  (k x : ℕ) → is-nonzero-ℕ k → (remainder-euclidean-division-ℕ k x) <-ℕ k
 strict-upper-bound-remainder-euclidean-division-ℕ k x =
   pr2 (pr2 (euclidean-division-ℕ k x))
 
diff --git a/src/elementary-number-theory/finitary-natural-numbers.lagda.md b/src/elementary-number-theory/finitary-natural-numbers.lagda.md
index f97fed792d..38cfb6ef99 100644
--- a/src/elementary-number-theory/finitary-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/finitary-natural-numbers.lagda.md
@@ -85,7 +85,7 @@ cong-unary-op-ℕ (succ-ℕ k) x n =
 
 ```agda
 le-constant-unary-op-ℕ :
-  (k : ℕ) (x y : Fin k) (m : ℕ) → le-ℕ (constant-ℕ k x) (unary-op-ℕ k y m)
+  (k : ℕ) (x y : Fin k) (m : ℕ) → (constant-ℕ k x) <-ℕ (unary-op-ℕ k y m)
 le-constant-unary-op-ℕ k x y m =
   concatenate-le-leq-ℕ {nat-Fin k x} {k} {unary-op-ℕ k y m}
     ( strict-upper-bound-nat-Fin k x)
diff --git a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
index 5f3f725db7..23c4cd02ef 100644
--- a/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
+++ b/src/elementary-number-theory/fundamental-theorem-of-arithmetic.lagda.md
@@ -152,7 +152,7 @@ Nontrivial divisors of a natural number are divisors strictly greater than `1`.
 
 ```agda
 is-nontrivial-divisor-ℕ : (n x : ℕ) → UU lzero
-is-nontrivial-divisor-ℕ n x = (le-ℕ 1 x) × (div-ℕ x n)
+is-nontrivial-divisor-ℕ n x = (1 <-ℕ x) × (div-ℕ x n)
 
 is-prop-is-nontrivial-divisor-ℕ :
   (n x : ℕ) → is-prop (is-nontrivial-divisor-ℕ n x)
@@ -171,7 +171,7 @@ is-decidable-is-nontrivial-divisor-ℕ n x =
   is-decidable-product (is-decidable-le-ℕ 1 x) (is-decidable-div-ℕ x n)
 
 is-nontrivial-divisor-diagonal-ℕ :
-  (n : ℕ) → le-ℕ 1 n → is-nontrivial-divisor-ℕ n n
+  (n : ℕ) → 1 <-ℕ n → is-nontrivial-divisor-ℕ n n
 pr1 (is-nontrivial-divisor-diagonal-ℕ n H) = H
 pr2 (is-nontrivial-divisor-diagonal-ℕ n H) = refl-div-ℕ n
 ```
@@ -277,29 +277,29 @@ is-list-of-nontrivial-divisors-is-prime-decomposition-list-ℕ x l D =
 
 ```agda
 least-nontrivial-divisor-ℕ :
-  (n : ℕ) → le-ℕ 1 n → minimal-element-ℕ (is-nontrivial-divisor-ℕ n)
+  (n : ℕ) → 1 <-ℕ n → minimal-element-ℕ (is-nontrivial-divisor-ℕ n)
 least-nontrivial-divisor-ℕ n H =
   well-ordering-principle-ℕ
     ( is-nontrivial-divisor-ℕ n)
     ( is-decidable-is-nontrivial-divisor-ℕ n)
     ( n , is-nontrivial-divisor-diagonal-ℕ n H)
 
-nat-least-nontrivial-divisor-ℕ : (n : ℕ) → le-ℕ 1 n → ℕ
+nat-least-nontrivial-divisor-ℕ : (n : ℕ) → 1 <-ℕ n → ℕ
 nat-least-nontrivial-divisor-ℕ n H = pr1 (least-nontrivial-divisor-ℕ n H)
 
 le-one-least-nontrivial-divisor-ℕ :
-  (n : ℕ) (H : le-ℕ 1 n) → le-ℕ 1 (nat-least-nontrivial-divisor-ℕ n H)
+  (n : ℕ) (H : 1 <-ℕ n) → 1 <-ℕ (nat-least-nontrivial-divisor-ℕ n H)
 le-one-least-nontrivial-divisor-ℕ n H =
   pr1 (pr1 (pr2 (least-nontrivial-divisor-ℕ n H)))
 
 div-least-nontrivial-divisor-ℕ :
-  (n : ℕ) (H : le-ℕ 1 n) → div-ℕ (nat-least-nontrivial-divisor-ℕ n H) n
+  (n : ℕ) (H : 1 <-ℕ n) → div-ℕ (nat-least-nontrivial-divisor-ℕ n H) n
 div-least-nontrivial-divisor-ℕ n H =
   pr2 (pr1 (pr2 (least-nontrivial-divisor-ℕ n H)))
 
 is-minimal-least-nontrivial-divisor-ℕ :
-  (n : ℕ) (H : le-ℕ 1 n) (x : ℕ) (K : le-ℕ 1 x) (d : div-ℕ x n) →
-  leq-ℕ (nat-least-nontrivial-divisor-ℕ n H) x
+  (n : ℕ) (H : 1 <-ℕ n) (x : ℕ) (K : 1 <-ℕ x) (d : div-ℕ x n) →
+  (nat-least-nontrivial-divisor-ℕ n H) ≤-ℕ x
 is-minimal-least-nontrivial-divisor-ℕ n H x K d =
   pr2 (pr2 (least-nontrivial-divisor-ℕ n H)) x (K , d)
 ```
@@ -309,7 +309,7 @@ is-minimal-least-nontrivial-divisor-ℕ n H x K d =
 ```agda
 abstract
   is-nonzero-least-nontrivial-divisor-ℕ :
-    (n : ℕ) (H : le-ℕ 1 n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
+    (n : ℕ) (H : 1 <-ℕ n) → is-nonzero-ℕ (nat-least-nontrivial-divisor-ℕ n H)
   is-nonzero-least-nontrivial-divisor-ℕ n H =
     is-nonzero-div-ℕ
       ( nat-least-nontrivial-divisor-ℕ n H)
@@ -322,11 +322,11 @@ abstract
 
 ```agda
 is-prime-least-nontrivial-divisor-ℕ :
-  (n : ℕ) (H : le-ℕ 1 n) → is-prime-ℕ (nat-least-nontrivial-divisor-ℕ n H)
+  (n : ℕ) (H : 1 <-ℕ n) → is-prime-ℕ (nat-least-nontrivial-divisor-ℕ n H)
 pr1 (is-prime-least-nontrivial-divisor-ℕ n H x) (K , L) =
   map-right-unit-law-coproduct-is-empty
     ( is-one-ℕ x)
-    ( le-ℕ 1 x)
+    ( 1 <-ℕ x)
     ( λ p →
       contradiction-le-ℕ x l
         ( le-div-ℕ x l
@@ -351,23 +351,23 @@ pr2 (pr2 (is-prime-least-nontrivial-divisor-ℕ n H .1) refl) =
 ### The least prime divisor of a number `1 < n`
 
 ```agda
-nat-least-prime-divisor-ℕ : (x : ℕ) → le-ℕ 1 x → ℕ
+nat-least-prime-divisor-ℕ : (x : ℕ) → 1 <-ℕ x → ℕ
 nat-least-prime-divisor-ℕ x H = nat-least-nontrivial-divisor-ℕ x H
 
 is-prime-least-prime-divisor-ℕ :
-  (x : ℕ) (H : le-ℕ 1 x) → is-prime-ℕ (nat-least-prime-divisor-ℕ x H)
+  (x : ℕ) (H : 1 <-ℕ x) → is-prime-ℕ (nat-least-prime-divisor-ℕ x H)
 is-prime-least-prime-divisor-ℕ x H = is-prime-least-nontrivial-divisor-ℕ x H
 
-least-prime-divisor-ℕ : (x : ℕ) → le-ℕ 1 x → Prime-ℕ
+least-prime-divisor-ℕ : (x : ℕ) → 1 <-ℕ x → Prime-ℕ
 pr1 (least-prime-divisor-ℕ x H) = nat-least-prime-divisor-ℕ x H
 pr2 (least-prime-divisor-ℕ x H) = is-prime-least-prime-divisor-ℕ x H
 
 div-least-prime-divisor-ℕ :
-  (x : ℕ) (H : le-ℕ 1 x) → div-ℕ (nat-least-prime-divisor-ℕ x H) x
+  (x : ℕ) (H : 1 <-ℕ x) → div-ℕ (nat-least-prime-divisor-ℕ x H) x
 div-least-prime-divisor-ℕ x H = div-least-nontrivial-divisor-ℕ x H
 
 quotient-div-least-prime-divisor-ℕ :
-  (x : ℕ) (H : le-ℕ 1 x) → ℕ
+  (x : ℕ) (H : 1 <-ℕ x) → ℕ
 quotient-div-least-prime-divisor-ℕ x H =
   quotient-div-ℕ
     ( nat-least-prime-divisor-ℕ x H)
@@ -375,7 +375,7 @@ quotient-div-least-prime-divisor-ℕ x H =
     ( div-least-prime-divisor-ℕ x H)
 
 leq-quotient-div-least-prime-divisor-ℕ :
-  (x : ℕ) (H : le-ℕ 1 (succ-ℕ x)) →
+  (x : ℕ) (H : 1 <-ℕ (succ-ℕ x)) →
   leq-ℕ (quotient-div-least-prime-divisor-ℕ (succ-ℕ x) H) x
 leq-quotient-div-least-prime-divisor-ℕ x H =
   leq-quotient-div-is-prime-ℕ
@@ -704,7 +704,7 @@ pr2 (prime-decomposition-fundamental-theorem-arithmetic-list-ℕ x H) =
 le-one-is-nonempty-prime-decomposition-list-ℕ :
   (x : ℕ) (H : leq-ℕ 1 x) (y : ℕ) (l : list ℕ) →
   is-prime-decomposition-list-ℕ x (cons y l) →
-  le-ℕ 1 x
+  1 <-ℕ x
 le-one-is-nonempty-prime-decomposition-list-ℕ x H y l D =
   concatenate-le-leq-ℕ
     {x = 1}
diff --git a/src/elementary-number-theory/goldbach-conjecture.lagda.md b/src/elementary-number-theory/goldbach-conjecture.lagda.md
index eef772ea6c..490589ef0d 100644
--- a/src/elementary-number-theory/goldbach-conjecture.lagda.md
+++ b/src/elementary-number-theory/goldbach-conjecture.lagda.md
@@ -26,6 +26,6 @@ open import foundation.universe-levels
 ```agda
 Goldbach-conjecture : UU lzero
 Goldbach-conjecture =
-  ( n : ℕ) → (le-ℕ 2 n) → (is-even-ℕ n) →
+  ( n : ℕ) → 2 <-ℕ n → is-even-ℕ n →
     Σ ℕ (λ p → (is-prime-ℕ p) × (Σ ℕ (λ q → (is-prime-ℕ q) × (p +ℕ q ＝ n))))
 ```
diff --git a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md b/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md
index 1a2639adb4..0c92c0bafe 100644
--- a/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/greatest-common-divisor-natural-numbers.lagda.md
@@ -232,7 +232,7 @@ div-gcd-is-common-divisor-ℕ a b x H with
 
 ```agda
 is-zero-is-common-divisor-le-gcd-ℕ :
-  (a b r : ℕ) → le-ℕ r (gcd-ℕ a b) →
+  (a b r : ℕ) → r <-ℕ gcd-ℕ a b →
   ((x : ℕ) → is-common-divisor-ℕ a b x → div-ℕ x r) → is-zero-ℕ r
 is-zero-is-common-divisor-le-gcd-ℕ a b r l d with is-decidable-is-zero-ℕ r
 ... | inl H = H
diff --git a/src/elementary-number-theory/inequality-natural-numbers.lagda.md b/src/elementary-number-theory/inequality-natural-numbers.lagda.md
index ec0f031359..54bc6f628c 100644
--- a/src/elementary-number-theory/inequality-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/inequality-natural-numbers.lagda.md
@@ -28,19 +28,24 @@ open import foundation.universe-levels
 
 open import order-theory.posets
 open import order-theory.preorders
+open import order-theory.total-orders
 ```
 
 </details>
 
 ## Idea
 
-The relation `≤` on the natural numbers is the unique relation such that `0` is
-less than any natural number, and such that `m+1 ≤ n+1` is equivalent to
-`m ≤ n`.
+The {{#concept "standard ordering relation" Agda=leq-ℕ}} on the
+[natural numbers](elementary-number-theory.natural-numbers.md) is the
+[unique](foundation-core.contractible-types.md)
+[relation](foundation.binary-relations.md) such that `0` is less than any
+natural number and such that `m + 1 ≤ n + 1` is
+[equivalent](foundation-core.equivalences.md) to `m ≤ n` for all natural numbers
+`m` and `n`.
 
 ## Definitions
 
-### The partial ordering on ℕ
+### The standard ordering relation on ℕ
 
 ```agda
 leq-ℕ : ℕ → ℕ → UU lzero
@@ -52,17 +57,19 @@ infix 30 _≤-ℕ_
 _≤-ℕ_ = leq-ℕ
 ```
 
-### Alternative definition of the partial ordering on ℕ
+### Alternative definition of the standard ordering relation on ℕ
 
 ```agda
 data leq-ℕ' : ℕ → ℕ → UU lzero where
   refl-leq-ℕ' : (n : ℕ) → leq-ℕ' n n
-  propagate-leq-ℕ' : {x y z : ℕ} → succ-ℕ y ＝ z → (leq-ℕ' x y) → (leq-ℕ' x z)
+  propagate-leq-ℕ' : {x y z : ℕ} → succ-ℕ y ＝ z → leq-ℕ' x y → leq-ℕ' x z
 ```
 
+It remains to formalize that this is equivalent to the conventional definition.
+
 ## Properties
 
-### Inequality on ℕ is a proposition
+### Inequality of natural numbers is a proposition
 
 ```agda
 is-prop-leq-ℕ :
@@ -77,7 +84,7 @@ pr1 (leq-ℕ-Prop m n) = leq-ℕ m n
 pr2 (leq-ℕ-Prop m n) = is-prop-leq-ℕ m n
 ```
 
-### The partial ordering on the natural numbers is decidable
+### Inequality is decidable
 
 ```agda
 is-decidable-leq-ℕ :
@@ -88,7 +95,7 @@ is-decidable-leq-ℕ (succ-ℕ m) zero-ℕ = inr id
 is-decidable-leq-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-leq-ℕ m n
 ```
 
-### The partial ordering on ℕ is a congruence
+### Inequality is a congruence
 
 ```agda
 concatenate-eq-leq-eq-ℕ :
@@ -104,7 +111,7 @@ concatenate-eq-leq-ℕ :
 concatenate-eq-leq-ℕ n refl H = H
 ```
 
-### Reflexivity
+### Inequality is reflexive
 
 ```agda
 refl-leq-ℕ : (n : ℕ) → n ≤-ℕ n
@@ -115,7 +122,7 @@ leq-eq-ℕ : (m n : ℕ) → m ＝ n → m ≤-ℕ n
 leq-eq-ℕ m .m refl = refl-leq-ℕ m
 ```
 
-### Transitivity
+### Inequality is transitive
 
 ```agda
 transitive-leq-ℕ : is-transitive leq-ℕ
@@ -124,7 +131,7 @@ transitive-leq-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
   transitive-leq-ℕ n m l p q
 ```
 
-### Antisymmetry
+### Inequality is antisymmetric
 
 ```agda
 antisymmetric-leq-ℕ : (m n : ℕ) → m ≤-ℕ n → n ≤-ℕ m → m ＝ n
@@ -133,7 +140,7 @@ antisymmetric-leq-ℕ (succ-ℕ m) (succ-ℕ n) p q =
   ap succ-ℕ (antisymmetric-leq-ℕ m n p q)
 ```
 
-### The poset of natural numbers
+### The preorder of natural numbers
 
 ```agda
 ℕ-Preorder : Preorder lzero lzero
@@ -141,7 +148,11 @@ pr1 ℕ-Preorder = ℕ
 pr1 (pr2 ℕ-Preorder) = leq-ℕ-Prop
 pr1 (pr2 (pr2 ℕ-Preorder)) = refl-leq-ℕ
 pr2 (pr2 (pr2 ℕ-Preorder)) = transitive-leq-ℕ
+```
 
+### The poset of natural numbers
+
+```agda
 ℕ-Poset : Poset lzero lzero
 pr1 ℕ-Poset = ℕ-Preorder
 pr2 ℕ-Poset = antisymmetric-leq-ℕ
@@ -196,7 +207,7 @@ leq-zero-ℕ :
 leq-zero-ℕ n = star
 ```
 
-### Any natural number less than zero is zero
+### Any natural number less than or equal to zero is zero
 
 ```agda
 is-zero-leq-zero-ℕ :
@@ -224,12 +235,12 @@ is-nonzero-leq-one-ℕ .zero-ℕ () refl
 ### Any natural number is less than or equal to its own successor
 
 ```agda
-succ-leq-ℕ : (n : ℕ) → n ≤-ℕ (succ-ℕ n)
+succ-leq-ℕ : (n : ℕ) → n ≤-ℕ succ-ℕ n
 succ-leq-ℕ zero-ℕ = star
 succ-leq-ℕ (succ-ℕ n) = succ-leq-ℕ n
 ```
 
-### An natural number less than `n+1` is either less than `n` or it is `n+1`
+### A natural number less than or equal to `n + 1` is either less than `n` or it is `n + 1`
 
 ```agda
 decide-leq-succ-ℕ :
@@ -242,11 +253,11 @@ decide-leq-succ-ℕ (succ-ℕ m) (succ-ℕ n) l =
   map-coproduct id (ap succ-ℕ) (decide-leq-succ-ℕ m n l)
 ```
 
-### If `m` is less than `n`, then it is less than `n+1`
+### If `m` is less than or equal to `n`, then it is less than or equal to `n + 1`
 
 ```agda
 preserves-leq-succ-ℕ :
-  (m n : ℕ) → m ≤-ℕ n → m ≤-ℕ (succ-ℕ n)
+  (m n : ℕ) → m ≤-ℕ n → m ≤-ℕ succ-ℕ n
 preserves-leq-succ-ℕ m n p = transitive-leq-ℕ m n (succ-ℕ n) (succ-leq-ℕ n) p
 ```
 
@@ -254,7 +265,7 @@ preserves-leq-succ-ℕ m n p = transitive-leq-ℕ m n (succ-ℕ n) (succ-leq-ℕ
 
 ```agda
 neg-succ-leq-ℕ :
-  (n : ℕ) → ¬ (leq-ℕ (succ-ℕ n) n)
+  (n : ℕ) → ¬ (succ-ℕ n ≤-ℕ n)
 neg-succ-leq-ℕ zero-ℕ = id
 neg-succ-leq-ℕ (succ-ℕ n) = neg-succ-leq-ℕ n
 ```
@@ -349,7 +360,7 @@ leq-add-ℕ' m n =
   concatenate-leq-eq-ℕ m (leq-add-ℕ m n) (commutative-add-ℕ m n)
 ```
 
-### We have `n ≤ m` if and only if there is a number `l` such that `l+n=m`
+### We have `n ≤ m` if and only if there is a number `l` such that `l + n = m`
 
 ```agda
 subtraction-leq-ℕ : (n m : ℕ) → n ≤-ℕ m → Σ ℕ (λ l → l +ℕ n ＝ m)
@@ -428,7 +439,7 @@ reflects-order-mul-ℕ' k m n H =
 
 ```agda
 leq-mul-ℕ :
-  (k x : ℕ) → x ≤-ℕ (x *ℕ (succ-ℕ k))
+  (k x : ℕ) → x ≤-ℕ (x *ℕ succ-ℕ k)
 leq-mul-ℕ k x =
   concatenate-eq-leq-ℕ
     ( x *ℕ (succ-ℕ k))
@@ -436,7 +447,7 @@ leq-mul-ℕ k x =
     ( preserves-order-mul-ℕ' x 1 (succ-ℕ k) (leq-zero-ℕ k))
 
 leq-mul-ℕ' :
-  (k x : ℕ) → x ≤-ℕ ((succ-ℕ k) *ℕ x)
+  (k x : ℕ) → x ≤-ℕ (succ-ℕ k *ℕ x)
 leq-mul-ℕ' k x =
   concatenate-leq-eq-ℕ x
     ( leq-mul-ℕ k x)
@@ -455,5 +466,7 @@ leq-mul-is-nonzero-ℕ' k x H with is-successor-is-nonzero-ℕ H
 
 ## See also
 
+- We show that the standard ordering is a decidable total order in
+  [`elementary-number-theory.decidable-total-order-natural-numbers`](elementary-number-theory.decidable-total-order-natural-numbers.md)
 - Strict inequality of the natural numbers is defined in
   [`strict-inequality-natural-numbers`](elementary-number-theory.strict-inequality-natural-numbers.md)
diff --git a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
index d21985ad6f..c9f9e3a707 100644
--- a/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
+++ b/src/elementary-number-theory/inequality-standard-finite-types.lagda.md
@@ -18,6 +18,7 @@ open import foundation.decidable-propositions
 open import foundation.decidable-types
 open import foundation.dependent-pair-types
 open import foundation.empty-types
+open import foundation.function-types
 open import foundation.identity-types
 open import foundation.propositions
 open import foundation.unit-type
@@ -85,7 +86,7 @@ leq-succ-Fin (succ-ℕ k) (inl x) = leq-succ-Fin k x
 leq-succ-Fin (succ-ℕ k) (inr star) = star
 
 preserves-leq-nat-Fin :
-  (k : ℕ) {x y : Fin k} → leq-Fin k x y → leq-ℕ (nat-Fin k x) (nat-Fin k y)
+  (k : ℕ) {x y : Fin k} → leq-Fin k x y → (nat-Fin k x) ≤-ℕ (nat-Fin k y)
 preserves-leq-nat-Fin (succ-ℕ k) {inl x} {inl y} H =
   preserves-leq-nat-Fin k H
 preserves-leq-nat-Fin (succ-ℕ k) {inl x} {inr star} H =
@@ -94,7 +95,7 @@ preserves-leq-nat-Fin (succ-ℕ k) {inr star} {inr star} H =
   refl-leq-ℕ k
 
 reflects-leq-nat-Fin :
-  (k : ℕ) {x y : Fin k} → leq-ℕ (nat-Fin k x) (nat-Fin k y) → leq-Fin k x y
+  (k : ℕ) {x y : Fin k} → (nat-Fin k x) ≤-ℕ (nat-Fin k y) → leq-Fin k x y
 reflects-leq-nat-Fin (succ-ℕ k) {inl x} {inl y} H =
   reflects-leq-nat-Fin k H
 reflects-leq-nat-Fin (succ-ℕ k) {inr star} {inl y} H =
@@ -126,7 +127,7 @@ pr2 (Fin-Poset k) = antisymmetric-leq-Fin k
 is-decidable-leq-Fin : (k : ℕ) (x y : Fin k) → is-decidable (leq-Fin k x y)
 is-decidable-leq-Fin (succ-ℕ k) (inl x) (inl y) = is-decidable-leq-Fin k x y
 is-decidable-leq-Fin (succ-ℕ k) (inl x) (inr y) = inl star
-is-decidable-leq-Fin (succ-ℕ k) (inr x) (inl y) = inr (λ x → x)
+is-decidable-leq-Fin (succ-ℕ k) (inr x) (inl y) = inr id
 is-decidable-leq-Fin (succ-ℕ k) (inr x) (inr y) = inl star
 
 leq-Fin-Decidable-Prop : (k : ℕ) → Fin k → Fin k → Decidable-Prop lzero
diff --git a/src/elementary-number-theory/infinitude-of-primes.lagda.md b/src/elementary-number-theory/infinitude-of-primes.lagda.md
index e106f39df4..e2555d187d 100644
--- a/src/elementary-number-theory/infinitude-of-primes.lagda.md
+++ b/src/elementary-number-theory/infinitude-of-primes.lagda.md
@@ -46,7 +46,7 @@ We begin by stating the infinitude of primes in type theory.
 
 ```agda
 Infinitude-Of-Primes-ℕ : UU lzero
-Infinitude-Of-Primes-ℕ = (n : ℕ) → Σ ℕ (λ p → is-prime-ℕ p × le-ℕ n p)
+Infinitude-Of-Primes-ℕ = (n : ℕ) → Σ ℕ (λ p → is-prime-ℕ p × n <-ℕ p)
 ```
 
 ## Theorem
@@ -77,7 +77,7 @@ is-one-is-divisor-below-larger-prime-ℕ :
 is-one-is-divisor-below-larger-prime-ℕ n =
   pr2 (in-sieve-of-eratosthenes-larger-prime-ℕ n)
 
-le-larger-prime-ℕ : (n : ℕ) → le-ℕ n (larger-prime-ℕ n)
+le-larger-prime-ℕ : (n : ℕ) → n <-ℕ larger-prime-ℕ n
 le-larger-prime-ℕ n = pr1 (in-sieve-of-eratosthenes-larger-prime-ℕ n)
 
 is-nonzero-larger-prime-ℕ : (n : ℕ) → is-nonzero-ℕ (larger-prime-ℕ n)
diff --git a/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md b/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md
index 80761f26c3..58499f7598 100644
--- a/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/ordinal-induction-natural-numbers.lagda.md
@@ -28,7 +28,7 @@ The computation rule should still be proven.
 ```agda
 □-<-ℕ :
   {l : Level} → (ℕ → UU l) → ℕ → UU l
-□-<-ℕ P n = (m : ℕ) → (le-ℕ m n) → P m
+□-<-ℕ P n = (m : ℕ) → m <-ℕ n → P m
 
 reflect-□-<-ℕ :
   {l : Level} (P : ℕ → UU l) →
diff --git a/src/elementary-number-theory/pisano-periods.lagda.md b/src/elementary-number-theory/pisano-periods.lagda.md
index d3d99b98ee..44192e79e1 100644
--- a/src/elementary-number-theory/pisano-periods.lagda.md
+++ b/src/elementary-number-theory/pisano-periods.lagda.md
@@ -136,7 +136,7 @@ has-ordered-repetition-fibonacci-pair-Fin k =
 
 is-ordered-repetition-fibonacci-pair-Fin : ℕ → ℕ → UU lzero
 is-ordered-repetition-fibonacci-pair-Fin k x =
-  Σ ℕ (λ y → (le-ℕ y x) × (fibonacci-pair-Fin k y ＝ fibonacci-pair-Fin k x))
+  Σ ℕ (λ y → (y <-ℕ x) × (fibonacci-pair-Fin k y ＝ fibonacci-pair-Fin k x))
 
 minimal-ordered-repetition-fibonacci-pair-Fin :
   (k : ℕ) → minimal-element-ℕ (is-ordered-repetition-fibonacci-pair-Fin k)
diff --git a/src/elementary-number-theory/prime-numbers.lagda.md b/src/elementary-number-theory/prime-numbers.lagda.md
index a7543fbf13..e74cc3a67e 100644
--- a/src/elementary-number-theory/prime-numbers.lagda.md
+++ b/src/elementary-number-theory/prime-numbers.lagda.md
@@ -111,7 +111,7 @@ is-not-one-is-prime-ℕ n H p = pr1 (pr2 (H 1) refl) (inv p)
 
 ```agda
 le-one-is-prime-ℕ :
-  (n : ℕ) → is-prime-ℕ n → le-ℕ 1 n
+  (n : ℕ) → is-prime-ℕ n → 1 <-ℕ n
 le-one-is-prime-ℕ 0 x = ex-falso (is-nonzero-is-prime-ℕ 0 x refl)
 le-one-is-prime-ℕ 1 x = ex-falso (is-not-one-is-prime-ℕ 1 x refl)
 le-one-is-prime-ℕ (succ-ℕ (succ-ℕ n)) x = star
@@ -226,7 +226,7 @@ is-prime-two-ℕ =
 ```agda
 le-quotient-div-is-prime-ℕ :
   (p x : ℕ) → is-nonzero-ℕ x → is-prime-ℕ p →
-  (H : div-ℕ p x) → le-ℕ (quotient-div-ℕ p x H) x
+  (H : div-ℕ p x) → quotient-div-ℕ p x H <-ℕ x
 le-quotient-div-is-prime-ℕ p x N P H =
   le-quotient-div-ℕ p x N H (is-not-one-is-prime-ℕ p P)
 ```
diff --git a/src/elementary-number-theory/proper-divisors-natural-numbers.lagda.md b/src/elementary-number-theory/proper-divisors-natural-numbers.lagda.md
index 0f35339378..f7e3745f17 100644
--- a/src/elementary-number-theory/proper-divisors-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/proper-divisors-natural-numbers.lagda.md
@@ -50,7 +50,7 @@ pr1 (is-proper-divisor-zero-succ-ℕ n) = is-nonzero-succ-ℕ n
 pr2 (is-proper-divisor-zero-succ-ℕ n) = div-zero-ℕ (succ-ℕ n)
 
 le-is-proper-divisor-ℕ :
-  (x y : ℕ) → is-nonzero-ℕ y → is-proper-divisor-ℕ y x → le-ℕ x y
+  (x y : ℕ) → is-nonzero-ℕ y → is-proper-divisor-ℕ y x → x <-ℕ y
 le-is-proper-divisor-ℕ x y H K =
   le-leq-neq-ℕ (leq-div-ℕ x y H (pr2 K)) (pr1 K)
 ```
@@ -84,11 +84,11 @@ pr2 (pr2 (is-proper-divisor-one-is-proper-divisor-ℕ {n} {x} H)) =
 ```agda
 le-one-quotient-div-is-proper-divisor-ℕ :
   (d x : ℕ) → is-nonzero-ℕ x → (H : div-ℕ d x) →
-  d ≠ x → le-ℕ 1 (quotient-div-ℕ d x H)
+  d ≠ x → 1 <-ℕ quotient-div-ℕ d x H
 le-one-quotient-div-is-proper-divisor-ℕ d x f H g =
   map-left-unit-law-coproduct-is-empty
     ( is-one-ℕ (quotient-div-ℕ d x H))
-    ( le-ℕ 1 (quotient-div-ℕ d x H))
+    ( 1 <-ℕ quotient-div-ℕ d x H)
     ( map-neg (eq-is-one-quotient-div-ℕ d x H) g)
     ( eq-or-le-leq-ℕ' 1
       ( quotient-div-ℕ d x H)
diff --git a/src/elementary-number-theory/sieve-of-eratosthenes.lagda.md b/src/elementary-number-theory/sieve-of-eratosthenes.lagda.md
index 1727176161..5324e34b0e 100644
--- a/src/elementary-number-theory/sieve-of-eratosthenes.lagda.md
+++ b/src/elementary-number-theory/sieve-of-eratosthenes.lagda.md
@@ -44,10 +44,10 @@ is-one-is-divisor-below-ℕ n a =
 
 in-sieve-of-eratosthenes-ℕ : ℕ → ℕ → UU lzero
 in-sieve-of-eratosthenes-ℕ n a =
-  (le-ℕ n a) × (is-one-is-divisor-below-ℕ n a)
+  (n <-ℕ a) × (is-one-is-divisor-below-ℕ n a)
 
 le-in-sieve-of-eratosthenes-ℕ :
-  (n a : ℕ) → in-sieve-of-eratosthenes-ℕ n a → le-ℕ n a
+  (n a : ℕ) → in-sieve-of-eratosthenes-ℕ n a → n <-ℕ a
 le-in-sieve-of-eratosthenes-ℕ n a = pr1
 ```
 
diff --git a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
index 86954ce090..9a40d1ba02 100644
--- a/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strict-inequality-natural-numbers.lagda.md
@@ -1,4 +1,4 @@
-# Strict inequality natural numbers
+# Strict inequality of natural numbers
 
 ```agda
 module elementary-number-theory.strict-inequality-natural-numbers where
@@ -12,6 +12,7 @@ open import elementary-number-theory.inequality-natural-numbers
 open import elementary-number-theory.natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.binary-relations
 open import foundation.cartesian-product-types
 open import foundation.coproduct-types
 open import foundation.decidable-types
@@ -52,19 +53,28 @@ _<-ℕ_ = le-ℕ
 
 ## Properties
 
+### If `x` is less than `y`, then `x` is less than or equal to `y`
+
+```agda
+leq-le-ℕ :
+  (x y : ℕ) → x <-ℕ y → x ≤-ℕ y
+leq-le-ℕ zero-ℕ (succ-ℕ y) H = star
+leq-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-ℕ x y H
+```
+
 ### Concatenating strict inequalities and equalities
 
 ```agda
 concatenate-eq-le-eq-ℕ :
-  {x y z w : ℕ} → x ＝ y → le-ℕ y z → z ＝ w → le-ℕ x w
+  {x y z w : ℕ} → x ＝ y → y <-ℕ z → z ＝ w → x <-ℕ w
 concatenate-eq-le-eq-ℕ refl p refl = p
 
 concatenate-eq-le-ℕ :
-  {x y z : ℕ} → x ＝ y → le-ℕ y z → le-ℕ x z
+  {x y z : ℕ} → x ＝ y → y <-ℕ z → x <-ℕ z
 concatenate-eq-le-ℕ refl p = p
 
 concatenate-le-eq-ℕ :
-  {x y z : ℕ} → le-ℕ x y → y ＝ z → le-ℕ x z
+  {x y z : ℕ} → x <-ℕ y → y ＝ z → x <-ℕ z
 concatenate-le-eq-ℕ p refl = p
 ```
 
@@ -72,7 +82,7 @@ concatenate-le-eq-ℕ p refl = p
 
 ```agda
 is-decidable-le-ℕ :
-  (m n : ℕ) → is-decidable (le-ℕ m n)
+  (m n : ℕ) → is-decidable (m <-ℕ n)
 is-decidable-le-ℕ zero-ℕ zero-ℕ = inr id
 is-decidable-le-ℕ zero-ℕ (succ-ℕ n) = inl star
 is-decidable-le-ℕ (succ-ℕ m) zero-ℕ = inr id
@@ -82,7 +92,7 @@ is-decidable-le-ℕ (succ-ℕ m) (succ-ℕ n) = is-decidable-le-ℕ m n
 ### If `m < n` then `n` must be nonzero
 
 ```agda
-is-nonzero-le-ℕ : (m n : ℕ) → le-ℕ m n → is-nonzero-ℕ n
+is-nonzero-le-ℕ : (m n : ℕ) → m <-ℕ n → is-nonzero-ℕ n
 is-nonzero-le-ℕ m .zero-ℕ () refl
 ```
 
@@ -98,7 +108,7 @@ le-is-nonzero-ℕ (succ-ℕ n) H = star
 
 ```agda
 contradiction-le-zero-ℕ :
-  (m : ℕ) → (le-ℕ m zero-ℕ) → empty
+  (m : ℕ) → (m <-ℕ zero-ℕ) → empty
 contradiction-le-zero-ℕ zero-ℕ ()
 contradiction-le-zero-ℕ (succ-ℕ m) ()
 ```
@@ -107,23 +117,23 @@ contradiction-le-zero-ℕ (succ-ℕ m) ()
 
 ```agda
 contradiction-le-one-ℕ :
-  (n : ℕ) → le-ℕ (succ-ℕ n) 1 → empty
+  (n : ℕ) → succ-ℕ n <-ℕ 1 → empty
 contradiction-le-one-ℕ zero-ℕ ()
 contradiction-le-one-ℕ (succ-ℕ n) ()
 ```
 
-### The strict ordering of the natural numbers is anti-reflexive
+### The strict ordering of the natural numbers is irreflexive
 
 ```agda
-anti-reflexive-le-ℕ : (n : ℕ) → ¬ (n <-ℕ n)
-anti-reflexive-le-ℕ zero-ℕ ()
-anti-reflexive-le-ℕ (succ-ℕ n) = anti-reflexive-le-ℕ n
+irreflexive-le-ℕ : is-irreflexive _<-ℕ_
+irreflexive-le-ℕ zero-ℕ ()
+irreflexive-le-ℕ (succ-ℕ n) = irreflexive-le-ℕ n
 ```
 
 ### If `x < y` then `x ≠ y`
 
 ```agda
-neq-le-ℕ : {x y : ℕ} → le-ℕ x y → x ≠ y
+neq-le-ℕ : {x y : ℕ} → x <-ℕ y → x ≠ y
 neq-le-ℕ {zero-ℕ} {succ-ℕ y} H = is-nonzero-succ-ℕ y ∘ inv
 neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ p)
 ```
@@ -131,7 +141,7 @@ neq-le-ℕ {succ-ℕ x} {succ-ℕ y} H p = neq-le-ℕ H (is-injective-succ-ℕ p
 ### Strict inequality is antisymmetric
 
 ```agda
-antisymmetric-le-ℕ : (m n : ℕ) → le-ℕ m n → le-ℕ n m → m ＝ n
+antisymmetric-le-ℕ : is-antisymmetric _<-ℕ_
 antisymmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q =
   ap succ-ℕ (antisymmetric-le-ℕ m n p q)
 ```
@@ -139,7 +149,7 @@ antisymmetric-le-ℕ (succ-ℕ m) (succ-ℕ n) p q =
 ### The strict ordering of the natural numbers is transitive
 
 ```agda
-transitive-le-ℕ : (n m l : ℕ) → (le-ℕ n m) → (le-ℕ m l) → (le-ℕ n l)
+transitive-le-ℕ : (n m l : ℕ) → n <-ℕ m → m <-ℕ l → n <-ℕ l
 transitive-le-ℕ zero-ℕ (succ-ℕ m) (succ-ℕ l) p q = star
 transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
   transitive-le-ℕ n m l p q
@@ -149,7 +159,7 @@ transitive-le-ℕ (succ-ℕ n) (succ-ℕ m) (succ-ℕ l) p q =
 
 ```agda
 transitive-le-ℕ' :
-  (k l m : ℕ) → (le-ℕ k l) → (le-ℕ l (succ-ℕ m)) → le-ℕ k m
+  (k l m : ℕ) → k <-ℕ l → l <-ℕ succ-ℕ m → k <-ℕ m
 transitive-le-ℕ' zero-ℕ zero-ℕ m () s
 transitive-le-ℕ' (succ-ℕ k) zero-ℕ m () s
 transitive-le-ℕ' zero-ℕ (succ-ℕ l) zero-ℕ star s =
@@ -164,7 +174,7 @@ transitive-le-ℕ' (succ-ℕ k) (succ-ℕ l) (succ-ℕ m) t s =
 ### Strict inequality is linear
 
 ```agda
-linear-le-ℕ : (x y : ℕ) → (le-ℕ x y) + ((x ＝ y) + (le-ℕ y x))
+linear-le-ℕ : (x y : ℕ) → (x <-ℕ y) + (x ＝ y) + (y <-ℕ x)
 linear-le-ℕ zero-ℕ zero-ℕ = inr (inl refl)
 linear-le-ℕ zero-ℕ (succ-ℕ y) = inl star
 linear-le-ℕ (succ-ℕ x) zero-ℕ = inr (inr star)
@@ -176,7 +186,7 @@ linear-le-ℕ (succ-ℕ x) (succ-ℕ y) =
 
 ```agda
 subtraction-le-ℕ :
-  (n m : ℕ) → le-ℕ n m → Σ ℕ (λ l → (is-nonzero-ℕ l) × (l +ℕ n ＝ m))
+  (n m : ℕ) → n <-ℕ m → Σ ℕ (λ l → (is-nonzero-ℕ l) × (l +ℕ n ＝ m))
 subtraction-le-ℕ zero-ℕ m p = pair m (pair (is-nonzero-le-ℕ zero-ℕ m p) refl)
 subtraction-le-ℕ (succ-ℕ n) (succ-ℕ m) p =
   pair (pr1 P) (pair (pr1 (pr2 P)) (ap succ-ℕ (pr2 (pr2 P))))
@@ -184,7 +194,7 @@ subtraction-le-ℕ (succ-ℕ n) (succ-ℕ m) p =
   P : Σ ℕ (λ l' → (is-nonzero-ℕ l') × (l' +ℕ n ＝ m))
   P = subtraction-le-ℕ n m p
 
-le-subtraction-ℕ : (n m l : ℕ) → is-nonzero-ℕ l → l +ℕ n ＝ m → le-ℕ n m
+le-subtraction-ℕ : (n m l : ℕ) → is-nonzero-ℕ l → l +ℕ n ＝ m → n <-ℕ m
 le-subtraction-ℕ zero-ℕ m l q p =
   tr (λ x → le-ℕ zero-ℕ x) p (le-is-nonzero-ℕ l q)
 le-subtraction-ℕ (succ-ℕ n) (succ-ℕ m) l q p =
@@ -194,7 +204,7 @@ le-subtraction-ℕ (succ-ℕ n) (succ-ℕ m) l q p =
 ### Any natural number is strictly less than its successor
 
 ```agda
-succ-le-ℕ : (n : ℕ) → le-ℕ n (succ-ℕ n)
+succ-le-ℕ : (n : ℕ) → n <-ℕ (succ-ℕ n)
 succ-le-ℕ zero-ℕ = star
 succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n
 ```
@@ -203,7 +213,7 @@ succ-le-ℕ (succ-ℕ n) = succ-le-ℕ n
 
 ```agda
 preserves-le-succ-ℕ :
-  (m n : ℕ) → le-ℕ m n → le-ℕ m (succ-ℕ n)
+  (m n : ℕ) → m <-ℕ n → m <-ℕ (succ-ℕ n)
 preserves-le-succ-ℕ m n H =
   transitive-le-ℕ m n (succ-ℕ n) H (succ-le-ℕ n)
 ```
@@ -212,14 +222,14 @@ preserves-le-succ-ℕ m n H =
 
 ```agda
 concatenate-leq-le-ℕ :
-  {x y z : ℕ} → x ≤-ℕ y → le-ℕ y z → le-ℕ x z
+  {x y z : ℕ} → x ≤-ℕ y → y <-ℕ z → x <-ℕ z
 concatenate-leq-le-ℕ {zero-ℕ} {zero-ℕ} {succ-ℕ z} H K = star
 concatenate-leq-le-ℕ {zero-ℕ} {succ-ℕ y} {succ-ℕ z} H K = star
 concatenate-leq-le-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
   concatenate-leq-le-ℕ {x} {y} {z} H K
 
 concatenate-le-leq-ℕ :
-  {x y z : ℕ} → le-ℕ x y → y ≤-ℕ z → le-ℕ x z
+  {x y z : ℕ} → x <-ℕ y → y ≤-ℕ z → x <-ℕ z
 concatenate-le-leq-ℕ {zero-ℕ} {succ-ℕ y} {succ-ℕ z} H K = star
 concatenate-le-leq-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
   concatenate-le-leq-ℕ {x} {y} {z} H K
@@ -228,7 +238,7 @@ concatenate-le-leq-ℕ {succ-ℕ x} {succ-ℕ y} {succ-ℕ z} H K =
 ### If `m < n` then `n ≰ m`
 
 ```agda
-contradiction-le-ℕ : (m n : ℕ) → le-ℕ m n → ¬ (n ≤-ℕ m)
+contradiction-le-ℕ : (m n : ℕ) → m <-ℕ n → ¬ (n ≤-ℕ m)
 contradiction-le-ℕ zero-ℕ (succ-ℕ n) H K = K
 contradiction-le-ℕ (succ-ℕ m) (succ-ℕ n) H = contradiction-le-ℕ m n H
 ```
@@ -236,34 +246,25 @@ contradiction-le-ℕ (succ-ℕ m) (succ-ℕ n) H = contradiction-le-ℕ m n H
 ### If `n ≤ m` then `m ≮ n`
 
 ```agda
-contradiction-le-ℕ' : (m n : ℕ) → n ≤-ℕ m → ¬ (le-ℕ m n)
+contradiction-le-ℕ' : (m n : ℕ) → n ≤-ℕ m → ¬ (m <-ℕ n)
 contradiction-le-ℕ' m n K H = contradiction-le-ℕ m n H K
 ```
 
 ### If `m ≮ n` then `n ≤ m`
 
 ```agda
-leq-not-le-ℕ : (m n : ℕ) → ¬ (le-ℕ m n) → n ≤-ℕ m
+leq-not-le-ℕ : (m n : ℕ) → ¬ (m <-ℕ n) → n ≤-ℕ m
 leq-not-le-ℕ zero-ℕ zero-ℕ H = star
 leq-not-le-ℕ zero-ℕ (succ-ℕ n) H = ex-falso (H star)
 leq-not-le-ℕ (succ-ℕ m) zero-ℕ H = star
 leq-not-le-ℕ (succ-ℕ m) (succ-ℕ n) H = leq-not-le-ℕ m n H
 ```
 
-### If `x < y` then `x ≤ y`
-
-```agda
-leq-le-ℕ :
-  (x y : ℕ) → le-ℕ x y → x ≤-ℕ y
-leq-le-ℕ zero-ℕ (succ-ℕ y) H = star
-leq-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-ℕ x y H
-```
-
 ### If `x < y + 1` then `x ≤ y`
 
 ```agda
 leq-le-succ-ℕ :
-  (x y : ℕ) → le-ℕ x (succ-ℕ y) → x ≤-ℕ y
+  (x y : ℕ) → x <-ℕ (succ-ℕ y) → x ≤-ℕ y
 leq-le-succ-ℕ zero-ℕ y H = star
 leq-le-succ-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-succ-ℕ x y H
 ```
@@ -272,7 +273,7 @@ leq-le-succ-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-le-succ-ℕ x y H
 
 ```agda
 leq-succ-le-ℕ :
-  (x y : ℕ) → le-ℕ x y → leq-ℕ (succ-ℕ x) y
+  (x y : ℕ) → x <-ℕ y → succ-ℕ x ≤-ℕ y
 leq-succ-le-ℕ zero-ℕ (succ-ℕ y) H = star
 leq-succ-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-succ-le-ℕ x y H
 ```
@@ -281,7 +282,7 @@ leq-succ-le-ℕ (succ-ℕ x) (succ-ℕ y) H = leq-succ-le-ℕ x y H
 
 ```agda
 le-succ-leq-ℕ :
-  (x y : ℕ) → leq-ℕ x y → le-ℕ x (succ-ℕ y)
+  (x y : ℕ) → leq-ℕ x y → x <-ℕ (succ-ℕ y)
 le-succ-leq-ℕ zero-ℕ zero-ℕ H = star
 le-succ-leq-ℕ zero-ℕ (succ-ℕ y) H = star
 le-succ-leq-ℕ (succ-ℕ x) (succ-ℕ y) H = le-succ-leq-ℕ x y H
@@ -291,18 +292,18 @@ le-succ-leq-ℕ (succ-ℕ x) (succ-ℕ y) H = le-succ-leq-ℕ x y H
 
 ```agda
 eq-or-le-leq-ℕ :
-  (x y : ℕ) → leq-ℕ x y → ((x ＝ y) + (le-ℕ x y))
+  (x y : ℕ) → leq-ℕ x y → (x ＝ y) + (x <-ℕ y)
 eq-or-le-leq-ℕ zero-ℕ zero-ℕ H = inl refl
 eq-or-le-leq-ℕ zero-ℕ (succ-ℕ y) H = inr star
 eq-or-le-leq-ℕ (succ-ℕ x) (succ-ℕ y) H =
   map-coproduct (ap succ-ℕ) id (eq-or-le-leq-ℕ x y H)
 
 eq-or-le-leq-ℕ' :
-  (x y : ℕ) → leq-ℕ x y → ((y ＝ x) + (le-ℕ x y))
+  (x y : ℕ) → leq-ℕ x y → (y ＝ x) + (x <-ℕ y)
 eq-or-le-leq-ℕ' x y H = map-coproduct inv id (eq-or-le-leq-ℕ x y H)
 
 leq-eq-or-le-ℕ :
-  (x y : ℕ) → ((x ＝ y) + (le-ℕ x y)) → leq-ℕ x y
+  (x y : ℕ) → (x ＝ y) + (x <-ℕ y) → leq-ℕ x y
 leq-eq-or-le-ℕ x .x (inl refl) = refl-leq-ℕ x
 leq-eq-or-le-ℕ x y (inr l) = leq-le-ℕ x y l
 ```
@@ -310,7 +311,7 @@ leq-eq-or-le-ℕ x y (inr l) = leq-le-ℕ x y l
 ### If `x ≤ y` and `x ≠ y` then `x < y`
 
 ```agda
-le-leq-neq-ℕ : {x y : ℕ} → x ≤-ℕ y → x ≠ y → le-ℕ x y
+le-leq-neq-ℕ : {x y : ℕ} → x ≤-ℕ y → x ≠ y → x <-ℕ y
 le-leq-neq-ℕ {zero-ℕ} {zero-ℕ} l f = ex-falso (f refl)
 le-leq-neq-ℕ {zero-ℕ} {succ-ℕ y} l f = star
 le-leq-neq-ℕ {succ-ℕ x} {succ-ℕ y} l f =
diff --git a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
index faab496e28..e0691e8c8b 100644
--- a/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strictly-ordered-pairs-of-natural-numbers.lagda.md
@@ -33,7 +33,7 @@ A strictly ordered pair of natural numbers consists of `x y : ℕ` such that
 
 ```agda
 strictly-ordered-pair-ℕ : UU lzero
-strictly-ordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → le-ℕ x y))
+strictly-ordered-pair-ℕ = Σ ℕ (λ x → Σ ℕ (λ y → x <-ℕ y))
 
 module _
   (p : strictly-ordered-pair-ℕ)
@@ -74,7 +74,7 @@ strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) zero-ℕ H =
   (0 , succ-ℕ a , star)
 strictly-ordered-pair-pair-of-distinct-elements-ℕ' (succ-ℕ a) (succ-ℕ b) H =
   map-Σ
-    ( λ x → Σ ℕ (λ y → le-ℕ x y))
+    ( λ x → Σ ℕ (λ y → x <-ℕ y))
     ( succ-ℕ)
     ( λ x →
       map-Σ (le-ℕ (succ-ℕ x)) succ-ℕ (λ y → id))
diff --git a/src/elementary-number-theory/strong-induction-natural-numbers.lagda.md b/src/elementary-number-theory/strong-induction-natural-numbers.lagda.md
index 5d18f2317f..0b007af326 100644
--- a/src/elementary-number-theory/strong-induction-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/strong-induction-natural-numbers.lagda.md
@@ -98,7 +98,7 @@ htpy-succ-strong-ind-ℕ P pS k H m p q =
 cases-eq-succ-strong-ind-ℕ :
   {l : Level} (P : ℕ → UU l) (pS : (k : ℕ) → (□-≤-ℕ P k) → P (succ-ℕ k)) →
   (k : ℕ) (H : □-≤-ℕ P k)
-  (c : (leq-ℕ (succ-ℕ k) k) + (succ-ℕ k ＝ succ-ℕ k)) →
+  (c : ((succ-ℕ k) ≤-ℕ k) + (succ-ℕ k ＝ succ-ℕ k)) →
   ( (cases-succ-strong-ind-ℕ P pS k H (succ-ℕ k) c)) ＝
   ( pS k H)
 cases-eq-succ-strong-ind-ℕ P pS k H (inl p) = ex-falso (neg-succ-leq-ℕ k p)
@@ -109,7 +109,7 @@ cases-eq-succ-strong-ind-ℕ P pS k H (inr α) =
 
 eq-succ-strong-ind-ℕ :
   {l : Level} (P : ℕ → UU l) (pS : (k : ℕ) → (□-≤-ℕ P k) → P (succ-ℕ k)) →
-  (k : ℕ) (H : □-≤-ℕ P k) (p : leq-ℕ (succ-ℕ k) (succ-ℕ k)) →
+  (k : ℕ) (H : □-≤-ℕ P k) (p : (succ-ℕ k) ≤-ℕ (succ-ℕ k)) →
   ( (succ-strong-ind-ℕ P pS k H (succ-ℕ k) p)) ＝
   ( pS k H)
 eq-succ-strong-ind-ℕ P pS k H p =
diff --git a/src/elementary-number-theory/sums-of-natural-numbers.lagda.md b/src/elementary-number-theory/sums-of-natural-numbers.lagda.md
index 494f4bbae3..0c0b023b8d 100644
--- a/src/elementary-number-theory/sums-of-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/sums-of-natural-numbers.lagda.md
@@ -63,7 +63,7 @@ sum-count-ℕ (pair k e) f = sum-Fin-ℕ k (f ∘ (map-equiv e))
 ### Bounded sums of natural numbers
 
 ```agda
-bounded-sum-ℕ : (u : ℕ) → ((x : ℕ) → le-ℕ x u → ℕ) → ℕ
+bounded-sum-ℕ : (u : ℕ) → ((x : ℕ) → x <-ℕ u → ℕ) → ℕ
 bounded-sum-ℕ zero-ℕ f = zero-ℕ
 bounded-sum-ℕ (succ-ℕ u) f =
   add-ℕ
@@ -112,6 +112,6 @@ abstract
 
 ```text
 leq-sum-Fin-ℕ :
-  {k : ℕ} (f : Fin k → ℕ) (x : Fin k) → leq-ℕ (f x) (sum-Fin-ℕ f)
+  {k : ℕ} (f : Fin k → ℕ) (x : Fin k) → (f x) ≤-ℕ (sum-Fin-ℕ f)
 leq-sum-Fin-ℕ {succ-ℕ k} f x = {!leq-add-ℕ!}
 ```
diff --git a/src/elementary-number-theory/taxicab-numbers.lagda.md b/src/elementary-number-theory/taxicab-numbers.lagda.md
index 78c1cc32bf..66a00a4693 100644
--- a/src/elementary-number-theory/taxicab-numbers.lagda.md
+++ b/src/elementary-number-theory/taxicab-numbers.lagda.md
@@ -63,7 +63,7 @@ sum-of-cubes-decomposition-ℕ x =
     ( λ y →
       Σ ( nonzero-ℕ)
         ( λ z →
-          ( leq-ℕ (nat-nonzero-ℕ y) (nat-nonzero-ℕ z)) ×
+          ( (nat-nonzero-ℕ y) ≤-ℕ (nat-nonzero-ℕ z)) ×
           ( cube-ℕ (nat-nonzero-ℕ y) +ℕ cube-ℕ (nat-nonzero-ℕ z) ＝ x)))
 ```
 
diff --git a/src/elementary-number-theory/upper-bounds-natural-numbers.lagda.md b/src/elementary-number-theory/upper-bounds-natural-numbers.lagda.md
index 2a0529164b..73285f9120 100644
--- a/src/elementary-number-theory/upper-bounds-natural-numbers.lagda.md
+++ b/src/elementary-number-theory/upper-bounds-natural-numbers.lagda.md
@@ -39,7 +39,7 @@ is-upper-bound-ℕ P n =
 is-strict-upper-bound-ℕ :
   {l : Level} (P : ℕ → UU l) (n : ℕ) → UU l
 is-strict-upper-bound-ℕ P n =
-  (m : ℕ) → P m → le-ℕ m n
+  (m : ℕ) → P m → m <-ℕ n
 ```
 
 ## Properties
diff --git a/src/finite-group-theory/orbits-permutations.lagda.md b/src/finite-group-theory/orbits-permutations.lagda.md
index 525f6e0278..b2cb0508e4 100644
--- a/src/finite-group-theory/orbits-permutations.lagda.md
+++ b/src/finite-group-theory/orbits-permutations.lagda.md
@@ -159,7 +159,7 @@ module _
       ( λ n →
         Σ ( ℕ)
           ( λ m →
-            ( le-ℕ m n) ×
+            ( m <-ℕ n) ×
             ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
   pr1 (two-points-iterate-ordered-ℕ (inl p)) = point2-iterate-ℕ
   pr1 (pr2 (two-points-iterate-ordered-ℕ (inl p))) = point1-iterate-ℕ
@@ -194,17 +194,17 @@ module _
         ( λ n →
           Σ ( ℕ)
             ( λ m →
-              ( le-ℕ m n) ×
+              ( m <-ℕ n) ×
               ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
     min-repeating =
       well-ordering-principle-ℕ
         ( λ n →
           Σ ( ℕ)
             ( λ m →
-              ( le-ℕ m n) ×
+              ( m <-ℕ n) ×
               ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
         ( λ n →
-          is-decidable-bounded-Σ-ℕ n ( λ m → le-ℕ m n)
+          is-decidable-bounded-Σ-ℕ n ( λ m → m <-ℕ n)
             ( λ m → Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))
             ( λ m → is-decidable-le-ℕ m n)
             ( λ m →
@@ -229,7 +229,7 @@ module _
         ( λ n →
           Σ ( ℕ)
             ( λ m →
-              ( le-ℕ m n) ×
+              ( m <-ℕ n) ×
               ( Id (iterate n (map-equiv f) a) (iterate m (map-equiv f) a))))
         ( first-point-min-repeating)
     is-lower-bound-min-reporting = pr2 (pr2 min-repeating)
@@ -275,10 +275,10 @@ module _
             ( pred-second)
             ( pair
               ( tr
-                ( λ x → le-ℕ (succ-ℕ pred-second) x)
+                ( λ x → succ-ℕ pred-second <-ℕ x)
                 ( equality-pred-first)
                 ( tr
-                  ( λ x → le-ℕ x first-point-min-repeating)
+                  ( λ x → x <-ℕ first-point-min-repeating)
                   ( equality-pred-second)
                   ( le-min-reporting)))
               ( is-injective-equiv
@@ -874,7 +874,7 @@ module _
       neq-iterate-nonzero-le-minimal-element :
         ( pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b))
         ( k : ℕ) →
-        ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa))) →
+        ( is-nonzero-ℕ k × (k <-ℕ pr1 (minimal-element-iterate g a b pa))) →
         ( iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element pa k (pair nz ineq)) q =
         contradiction-le-ℕ
@@ -909,7 +909,7 @@ module _
             ineq (pr2 (pr2 (minimal-element-iterate g a b pa)) k r))
       equal-iterate-transposition-a :
         (pa : Σ ℕ (λ k → Id (iterate k (map-equiv g) a) b)) (k : ℕ) →
-        le-ℕ k (pr1 (minimal-element-iterate g a b pa)) →
+        k <-ℕ pr1 (minimal-element-iterate g a b pa) →
         ( Id
           ( iterate k (map-equiv (composition-transposition-a-b g)) a)
           ( iterate k (map-equiv g) a))
@@ -933,7 +933,7 @@ module _
         cases-equal-iterate-transposition-a :
           is-decidable (is-zero-ℕ k) →
           ( is-zero-ℕ k) +
-          ( is-nonzero-ℕ k × le-ℕ k (pr1 (minimal-element-iterate g a b pa)))
+          ( is-nonzero-ℕ k × (k <-ℕ pr1 (minimal-element-iterate g a b pa)))
         cases-equal-iterate-transposition-a (inl s) = inl s
         cases-equal-iterate-transposition-a (inr s) = inr (pair s ineq)
       lemma2 :
@@ -1054,7 +1054,7 @@ module _
           quotient-euclidean-division-ℕ
             ( pr1 (minimal-element-iterate g a b pa))
             ( k)
-        ineq : le-ℕ r (pr1 (minimal-element-iterate g a b pa))
+        ineq : r <-ℕ pr1 (minimal-element-iterate g a b pa)
         ineq =
           strict-upper-bound-remainder-euclidean-division-ℕ
             ( pr1 (minimal-element-iterate g a b pa))
@@ -1166,7 +1166,7 @@ module _
               ( Id (iterate k (map-equiv g) x) a) +
               ( Id (iterate k (map-equiv g) x) b)))
         ( k : ℕ) →
-        ( le-ℕ k (pr1 (minimal-element-iterate-2-a-b g pa))) →
+        ( k <-ℕ pr1 (minimal-element-iterate-2-a-b g pa)) →
         Id
           ( iterate k (map-equiv (composition-transposition-a-b g)) x)
           ( iterate k (map-equiv g) x)
@@ -2185,7 +2185,7 @@ module _
           ( has-finite-orbits-permutation X eX g a)
       neq-iterate-nonzero-le-minimal-element :
         (k : ℕ) →
-        is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating) →
+        is-nonzero-ℕ k × (k <-ℕ pr1 minimal-element-iterate-repeating) →
         (iterate k (map-equiv g) a ≠ a) × (iterate k (map-equiv g) a ≠ b)
       pr1 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) Q =
         contradiction-le-ℕ k (pr1 minimal-element-iterate-repeating) ineq
@@ -2193,7 +2193,7 @@ module _
       pr2 (neq-iterate-nonzero-le-minimal-element k (pair nz ineq)) R =
         NP (unit-trunc-Prop (pair k R))
       equal-iterate-transposition-a :
-        (k : ℕ) → le-ℕ k (pr1 minimal-element-iterate-repeating) →
+        (k : ℕ) → k <-ℕ pr1 minimal-element-iterate-repeating →
         Id
           ( iterate k (map-equiv (composition-transposition-a-b g)) a)
           ( iterate k (map-equiv g) a)
@@ -2218,7 +2218,7 @@ module _
         cases-equal-iterate-transposition-a :
           is-decidable (is-zero-ℕ k) →
           ( is-zero-ℕ k) +
-          ( is-nonzero-ℕ k × le-ℕ k (pr1 minimal-element-iterate-repeating))
+          ( is-nonzero-ℕ k × (k <-ℕ pr1 minimal-element-iterate-repeating))
         cases-equal-iterate-transposition-a (inl s) = inl s
         cases-equal-iterate-transposition-a (inr s) = inr (pair s ineq)
       lemma :
diff --git a/src/lists/quicksort-lists.lagda.md b/src/lists/quicksort-lists.lagda.md
index d78ed47545..8503bc07c0 100644
--- a/src/lists/quicksort-lists.lagda.md
+++ b/src/lists/quicksort-lists.lagda.md
@@ -129,7 +129,7 @@ module _
       succ-leq-ℕ (length-list l)
 
     inequality-length-quicksort-list-divide-strict-greater :
-      (x : type-Decidable-Total-Order X) →
+      (x : type-Decidable-Total-Order X) →
       (l : list (type-Decidable-Total-Order X)) →
       length-list (quicksort-list-divide-strict-greater x l) ≤-ℕ length-list l
     inequality-length-quicksort-list-divide-strict-greater x nil = star
diff --git a/src/univalent-combinatorics/classical-finite-types.lagda.md b/src/univalent-combinatorics/classical-finite-types.lagda.md
index 1f7ddfffdd..9e09e98f99 100644
--- a/src/univalent-combinatorics/classical-finite-types.lagda.md
+++ b/src/univalent-combinatorics/classical-finite-types.lagda.md
@@ -32,7 +32,7 @@ i.e., it is the type of natural numbers strictly less than n.
 
 ```agda
 classical-Fin : ℕ → UU lzero
-classical-Fin k = Σ ℕ (λ x → le-ℕ x k)
+classical-Fin k = Σ ℕ (λ x → x <-ℕ k)
 ```
 
 ### The inclusion from `classical-Fin` to ℕ
diff --git a/src/univalent-combinatorics/pigeonhole-principle.lagda.md b/src/univalent-combinatorics/pigeonhole-principle.lagda.md
index 97927d8ab5..b091327c86 100644
--- a/src/univalent-combinatorics/pigeonhole-principle.lagda.md
+++ b/src/univalent-combinatorics/pigeonhole-principle.lagda.md
@@ -75,7 +75,7 @@ leq-is-injective-Fin k l H =
 
 ```agda
 is-not-emb-le-Fin :
-  (k l : ℕ) (f : Fin k → Fin l) → le-ℕ l k → ¬ (is-emb f)
+  (k l : ℕ) (f : Fin k → Fin l) → l <-ℕ k → ¬ (is-emb f)
 is-not-emb-le-Fin k l f p =
   map-neg (leq-is-emb-Fin k l) (contradiction-le-ℕ l k p)
 ```
@@ -84,7 +84,7 @@ is-not-emb-le-Fin k l f p =
 
 ```agda
 is-not-injective-le-Fin :
-  (k l : ℕ) (f : Fin k → Fin l) → le-ℕ l k → is-not-injective f
+  (k l : ℕ) (f : Fin k → Fin l) → l <-ℕ k → is-not-injective f
 is-not-injective-le-Fin k l f p =
   map-neg (is-emb-is-injective (is-set-Fin l)) (is-not-emb-le-Fin k l f p)
 ```
@@ -113,7 +113,7 @@ no-embedding-ℕ-Fin k e =
 
 ```agda
 module _
-  (k l : ℕ) (f : Fin k → Fin l) (p : le-ℕ l k)
+  (k l : ℕ) (f : Fin k → Fin l) (p : l <-ℕ k)
   where
 
   repetition-of-values-le-Fin : repetition-of-values f
@@ -197,7 +197,7 @@ module _
 ```agda
   is-not-emb-le-count :
     (f : A → B) →
-    le-ℕ (number-of-elements-count eB) (number-of-elements-count eA) →
+    (number-of-elements-count eB) <-ℕ (number-of-elements-count eA) →
     ¬ (is-emb f)
   is-not-emb-le-count f p H =
     is-not-emb-le-Fin
@@ -218,7 +218,7 @@ module _
 ```agda
   is-not-injective-le-count :
     (f : A → B) →
-    le-ℕ (number-of-elements-count eB) (number-of-elements-count eA) →
+    (number-of-elements-count eB) <-ℕ (number-of-elements-count eA) →
     is-not-injective f
   is-not-injective-le-count f p H =
     is-not-emb-le-count f p (is-emb-is-injective (is-set-count eB) H)
@@ -241,7 +241,7 @@ no-embedding-ℕ-count e f =
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (eA : count A) (eB : count B)
   (f : A → B)
-  (p : le-ℕ (number-of-elements-count eB) (number-of-elements-count eA))
+  (p : (number-of-elements-count eB) <-ℕ (number-of-elements-count eA))
   where
 
   repetition-of-values-le-count : repetition-of-values f
@@ -338,7 +338,7 @@ module _
 ```agda
   is-not-emb-le-is-finite :
     (f : A → B) →
-    le-ℕ (number-of-elements-is-finite K) (number-of-elements-is-finite H) →
+    (number-of-elements-is-finite K) <-ℕ (number-of-elements-is-finite H) →
     ¬ (is-emb f)
   is-not-emb-le-is-finite f p E =
     apply-universal-property-trunc-Prop H empty-Prop
@@ -357,7 +357,7 @@ module _
 ```agda
   is-not-injective-le-is-finite :
     (f : A → B) →
-    le-ℕ (number-of-elements-is-finite K) (number-of-elements-is-finite H) →
+    (number-of-elements-is-finite K) <-ℕ (number-of-elements-is-finite H) →
     is-not-injective f
   is-not-injective-le-is-finite f p I =
     is-not-emb-le-is-finite f p (is-emb-is-injective (is-set-is-finite K) I)
diff --git a/src/univalent-combinatorics/sequences-finite-types.lagda.md b/src/univalent-combinatorics/sequences-finite-types.lagda.md
index b9d113365b..85d0da7ae6 100644
--- a/src/univalent-combinatorics/sequences-finite-types.lagda.md
+++ b/src/univalent-combinatorics/sequences-finite-types.lagda.md
@@ -83,7 +83,7 @@ is-repetition-pair-of-distinct-elements-repetition-of-values-sequence-Fin k f =
 
 le-first-repetition-of-values-sequence-Fin :
   (k : ℕ) (f : sequence (Fin k)) →
-  le-ℕ (first-repetition-of-values-sequence-Fin k f) (succ-ℕ k)
+  (first-repetition-of-values-sequence-Fin k f) <-ℕ (succ-ℕ k)
 le-first-repetition-of-values-sequence-Fin k f =
   strict-upper-bound-nat-Fin
     ( succ-ℕ k)
@@ -126,10 +126,10 @@ ordered-repetition-of-values-nat-to-count e f =
 
 minimal-element-repetition-of-values-sequence-Fin :
   (k : ℕ) (f : ℕ → Fin k) →
-  minimal-element-ℕ (λ x → Σ ℕ (λ y → (le-ℕ y x) × (f y ＝ f x)))
+  minimal-element-ℕ (λ x → Σ ℕ (λ y → (y <-ℕ x) × (f y ＝ f x)))
 minimal-element-repetition-of-values-sequence-Fin k f =
   well-ordering-principle-ℕ
-    ( λ x → Σ ℕ (λ y → (le-ℕ y x) × (Id (f y) (f x))))
+    ( λ x → Σ ℕ (λ y → (y <-ℕ x) × (f y ＝ f x)))
     ( λ x →
       is-decidable-strictly-bounded-Σ-ℕ' x
         ( λ y → f y ＝ f x)
@@ -144,7 +144,7 @@ minimal-element-repetition-of-values-sequence-Fin k f =
 
 minimal-element-repetition-of-values-sequence-count :
   {l : Level} {A : UU l} (e : count A) (f : ℕ → A) →
-  minimal-element-ℕ (λ x → Σ ℕ (λ y → (le-ℕ y x) × (f y ＝ f x)))
+  minimal-element-ℕ (λ x → Σ ℕ (λ y → (y <-ℕ x) × (f y ＝ f x)))
 minimal-element-repetition-of-values-sequence-count (k , e) f =
   ( ( n) ,
     ( ( u) ,
diff --git a/src/univalent-combinatorics/standard-finite-types.lagda.md b/src/univalent-combinatorics/standard-finite-types.lagda.md
index 9756d21d09..164034690b 100644
--- a/src/univalent-combinatorics/standard-finite-types.lagda.md
+++ b/src/univalent-combinatorics/standard-finite-types.lagda.md
@@ -191,7 +191,7 @@ nat-Fin-reverse : (k : ℕ) → Fin k → ℕ
 nat-Fin-reverse (succ-ℕ k) (inl x) = succ-ℕ (nat-Fin k x)
 nat-Fin-reverse (succ-ℕ k) (inr x) = 0
 
-strict-upper-bound-nat-Fin : (k : ℕ) (x : Fin k) → le-ℕ (nat-Fin k x) k
+strict-upper-bound-nat-Fin : (k : ℕ) (x : Fin k) → (nat-Fin k x) <-ℕ k
 strict-upper-bound-nat-Fin (succ-ℕ k) (inl x) =
   transitive-le-ℕ
     ( nat-Fin k x)
@@ -210,7 +210,7 @@ upper-bound-nat-Fin (succ-ℕ k) (inl x) =
 upper-bound-nat-Fin (succ-ℕ k) (inr star) = refl-leq-ℕ (succ-ℕ k)
 
 upper-bound-nat-Fin' :
-  (k : ℕ) (x : Fin k) → leq-ℕ (nat-Fin k x) k
+  (k : ℕ) (x : Fin k) → (nat-Fin k x) ≤-ℕ k
 upper-bound-nat-Fin' k x =
   leq-le-ℕ (nat-Fin k x) k (strict-upper-bound-nat-Fin k x)