diff --git a/Cubical/Algebra/AbGroup/Instances/Fast/Int.agda b/Cubical/Algebra/AbGroup/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..262535dcb3
--- /dev/null
+++ b/Cubical/Algebra/AbGroup/Instances/Fast/Int.agda
@@ -0,0 +1,9 @@
+module Cubical.Algebra.AbGroup.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Fast.Int
+open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Group.Instances.Fast.Int
+
+ℤAbGroup : AbGroup ℓ-zero
+ℤAbGroup = Group→AbGroup ℤGroup +Comm
diff --git a/Cubical/Algebra/CommRing/Instances/Fast/Int.agda b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..e01dde2d62
--- /dev/null
+++ b/Cubical/Algebra/CommRing/Instances/Fast/Int.agda
@@ -0,0 +1,23 @@
+module Cubical.Algebra.CommRing.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Data.Fast.Int as Int renaming (_+_ to _+ℤ_; _·_ to _·ℤ_ ; -_ to -ℤ_)
+
+open CommRingStr using (0r ; 1r ; _+_ ; _·_ ; -_ ; isCommRing)
+
+ℤCommRing : CommRing ℓ-zero
+fst ℤCommRing = ℤ
+0r (snd ℤCommRing) = pos 0
+1r (snd ℤCommRing) = pos 1
+_+_ (snd ℤCommRing) = _+ℤ_
+_·_ (snd ℤCommRing) = _·ℤ_
+- snd ℤCommRing = -ℤ_
+isCommRing (snd ℤCommRing) = isCommRingℤ
+  where
+  abstract
+    isCommRingℤ : IsCommRing (pos 0) (pos 1) _+ℤ_ _·ℤ_ -ℤ_
+    isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc +IdR
+                                 -Cancel Int.+Comm Int.·Assoc
+                                 Int.·IdR ·DistR+ Int.·Comm
diff --git a/Cubical/Algebra/Group/Instances/Fast/Int.agda b/Cubical/Algebra/Group/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..60cdc00788
--- /dev/null
+++ b/Cubical/Algebra/Group/Instances/Fast/Int.agda
@@ -0,0 +1,56 @@
+module Cubical.Algebra.Group.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+
+open import Cubical.Data.Fast.Int renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_ ; _·_ to _·ℤ_ ; -_ to -ℤ_)
+
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+open import Cubical.Data.Fin.Base
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+
+
+open GroupStr
+
+ℤGroup : Group₀
+fst ℤGroup = ℤ
+1g (snd ℤGroup) = 0
+_·_ (snd ℤGroup) = _+ℤ_
+inv (snd ℤGroup) = -ℤ_
+isGroup (snd ℤGroup) = isGroupℤ
+  where
+  abstract
+    isGroupℤ : IsGroup (pos 0) (_+ℤ_) (-ℤ_)
+    isGroupℤ = makeIsGroup isSetℤ
+                           +Assoc +IdR +IdL
+                           -Cancel -Cancel'
+
+ℤHom : (n : ℤ) → GroupHom ℤGroup ℤGroup
+fst (ℤHom n) x = n ·ℤ x
+snd (ℤHom n) =
+  makeIsGroupHom λ x y → ·DistR+ n x y
+
+negEquivℤ : GroupEquiv ℤGroup ℤGroup
+fst negEquivℤ =
+  isoToEquiv
+    (iso (GroupStr.inv (snd ℤGroup))
+         (GroupStr.inv (snd ℤGroup))
+         (GroupTheory.invInv ℤGroup)
+         (GroupTheory.invInv ℤGroup))
+snd negEquivℤ =
+  makeIsGroupHom -Dist+
+
+sumFinGroupℤComm : (G : Group₀) (h : GroupIso G ℤGroup) {n : ℕ}
+  (f : Fin n → fst G) → sumFinℤ {n = n} (λ a → Iso.fun (fst h) (f a))
+  ≡ Iso.fun (fst h) (sumFinGroup G {n = n} f)
+sumFinGroupℤComm G h {n = zero} f = sym (IsGroupHom.pres1 (snd h))
+sumFinGroupℤComm G h {n = suc n} f =
+    cong₂ _+ℤ_ (λ _ → Iso.fun (fst h) (f flast))
+      (sumFinGroupℤComm G h {n = n} (f ∘ injectSuc {n = n}))
+  ∙ sym (IsGroupHom.pres· (snd h) (f flast)
+    (sumFinGroup G {n = n} (λ x → f (injectSuc {n = n} x))))
diff --git a/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..45a38d41c6
--- /dev/null
+++ b/Cubical/Algebra/OrderedCommRing/Instances/Fast/Int.agda
@@ -0,0 +1,66 @@
+module Cubical.Algebra.OrderedCommRing.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Empty as ⊥
+
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Fast.Int as ℤ
+  renaming (_+_ to _+ℤ_ ; _-_ to _-ℤ_; -_ to -ℤ_ ; _·_ to _·ℤ_)
+open import Cubical.Data.Fast.Int.Order
+  renaming (_<_ to _<ℤ_ ; _≤_ to _≤ℤ_)
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Fast.Int
+
+open import Cubical.Algebra.OrderedCommRing
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Fast.Int
+
+open import Cubical.Relation.Binary.Order.Pseudolattice
+open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Fast.Int
+
+open import Cubical.Relation.Binary
+open BinaryRelation
+
+open CommRingStr
+open OrderedCommRingStr
+open PseudolatticeStr
+open StrictOrderStr
+
+ℤOrderedCommRing : OrderedCommRing ℓ-zero ℓ-zero
+fst ℤOrderedCommRing = ℤ
+0r  (snd ℤOrderedCommRing) = 0
+1r  (snd ℤOrderedCommRing) = 1
+_+_ (snd ℤOrderedCommRing) = _+ℤ_
+_·_ (snd ℤOrderedCommRing) = _·ℤ_
+-_  (snd ℤOrderedCommRing) = -ℤ_
+_<_ (snd ℤOrderedCommRing) = _<ℤ_
+_≤_ (snd ℤOrderedCommRing) = _≤ℤ_
+isOrderedCommRing (snd ℤOrderedCommRing) = isOrderedCommRingℤ
+  where
+    open IsOrderedCommRing
+
+    isOrderedCommRingℤ : IsOrderedCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_ _<ℤ_ _≤ℤ_
+    isOrderedCommRingℤ .isCommRing      = ℤCommRing .snd .isCommRing
+    isOrderedCommRingℤ .isPseudolattice = ℤ≤Pseudolattice .snd .is-pseudolattice
+    isOrderedCommRingℤ .isStrictOrder   = ℤ<StrictOrder .snd .isStrictOrder
+    isOrderedCommRingℤ .<-≤-weaken      = λ _ _ → <-weaken
+    isOrderedCommRingℤ .≤≃¬>            = λ x y →
+      propBiimpl→Equiv isProp≤ (isProp¬ (y <ℤ x))
+        (λ x≤y y<x → isIrrefl< (≤<-trans x≤y y<x))
+        isAsym'<
+    isOrderedCommRingℤ .+MonoR≤         = λ _ _ _ → ≤-+o
+    isOrderedCommRingℤ .+MonoR<         = λ _ _ _ → <-+o
+    isOrderedCommRingℤ .posSum→pos∨pos  = λ _ _ → ∣_∣₁ ∘ 0<+ _ _
+    isOrderedCommRingℤ .<-≤-trans       = λ _ _ _ → <≤-trans
+    isOrderedCommRingℤ .≤-<-trans       = λ _ _ _ → ≤<-trans
+    isOrderedCommRingℤ .·MonoR≤         = λ _ _ _ → 0≤o→≤-·o
+    isOrderedCommRingℤ .·MonoR<         = λ _ _ _ → 0<o→<-·o
+    isOrderedCommRingℤ .0<1             = zero-<possuc
diff --git a/Cubical/Data/Fast/Int.agda b/Cubical/Data/Fast/Int.agda
new file mode 100644
index 0000000000..9b344a0889
--- /dev/null
+++ b/Cubical/Data/Fast/Int.agda
@@ -0,0 +1,6 @@
+-- This is the fast version of the integers.
+-- It uses the preferred version of the integers, but with more efficient operations.
+module Cubical.Data.Fast.Int where
+
+open import Cubical.Data.Fast.Int.Base public
+open import Cubical.Data.Fast.Int.Properties public
diff --git a/Cubical/Data/Fast/Int/Base.agda b/Cubical/Data/Fast/Int/Base.agda
new file mode 100644
index 0000000000..900210de09
--- /dev/null
+++ b/Cubical/Data/Fast/Int/Base.agda
@@ -0,0 +1,40 @@
+module Cubical.Data.Fast.Int.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_)
+open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_ ; sumFinℤ ; sumFinℤId) public
+open import Cubical.Data.Fin.Base
+
+infixl 7 _·_
+infixl 6 _+_ _-_
+
+ℕ-hlp : ℕ → ℕ → ℤ
+ℕ-hlp m-n@zero n-m = - (pos n-m)
+ℕ-hlp m-n@(suc _) n-m = pos m-n
+
+_ℕ-_ : ℕ → ℕ → ℤ
+m ℕ- n = ℕ-hlp (m ℕ.∸ n) (n ℕ.∸ m)
+
+_+_ : ℤ → ℤ → ℤ
+pos m    + pos n    = pos (m ℕ.+ n)
+negsuc m + negsuc n = negsuc (suc (m ℕ.+ n))
+pos m    + negsuc n = m ℕ- (suc n)
+negsuc m + pos n    = n ℕ- (suc m)
+
+_-_ : ℤ → ℤ → ℤ
+m - n = m + (- n)
+
+_·_ : ℤ → ℤ → ℤ
+pos m       · pos n       = pos (m ℕ.· n)
+pos zero    · negsuc n    = pos zero
+pos (suc m) · negsuc n    = negsuc (predℕ (suc m ℕ.· suc n))
+negsuc m    · pos zero    = pos zero
+negsuc m    · pos (suc n) = negsuc (predℕ (suc m ℕ.· suc n))
+negsuc m    · negsuc n    = pos (suc m ℕ.· suc n)
+
+sumFinℤ : {n : ℕ} (f : Fin n → ℤ) → ℤ
+sumFinℤ {n = n} f = sumFinGen {n = n} _+_ 0 f
+
+sumFinℤId : (n : ℕ) {f g : Fin n → ℤ}
+  → ((x : _) → f x ≡ g x) → sumFinℤ {n = n} f ≡ sumFinℤ {n = n} g
+sumFinℤId n t i = sumFinℤ {n = n} λ x → t x i
diff --git a/Cubical/Data/Fast/Int/Divisibility.agda b/Cubical/Data/Fast/Int/Divisibility.agda
new file mode 100644
index 0000000000..77d0da8176
--- /dev/null
+++ b/Cubical/Data/Fast/Int/Divisibility.agda
@@ -0,0 +1,438 @@
+{-
+
+Base facts about that the ring ℤ is Bézout domain
+
+-}
+module Cubical.Data.Fast.Int.Divisibility where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Data.Nat
+  hiding   (+-assoc ; +-comm ; ·-comm)
+  renaming (_·_ to _·ℕ_; _+_ to _+ℕ_ ; ·-assoc to ·ℕ-assoc)
+open import Cubical.Data.Nat.Order
+open import Cubical.Data.Nat.Divisibility
+  using    (m∣n→m≤n)
+  renaming (_∣_ to _∣ℕ_ ; isProp∣ to isProp∣ℕ ; stDivIneq to stDivIneqℕ)
+open import Cubical.Data.Nat.Mod
+open import Cubical.Data.Fast.Int.Base as ℤ
+  hiding   (_+_ ; _·_ ; _-_ ; -_)
+open import Cubical.Data.Fast.Int.Properties as ℤ
+  hiding (addEq ; ·Comm ; ·Assoc ; +Comm ; +Assoc ; ·DistL+)
+
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+
+open import Cubical.HITs.PropositionalTruncation as Prop
+open import Cubical.Relation.Nullary
+
+open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Instances.Fast.Int
+open import Cubical.Tactics.CommRingSolver
+
+private
+  variable
+    m n k : ℤ
+
+
+open CommRingStr      (ℤCommRing .snd)
+
+-- The Divisibility Relation
+-- Most definitions are the same as in Cubical.Data.Nat.Divisibility
+
+_∣_ : ℤ → ℤ → Type
+m ∣ n = ∃[ c ∈ ℤ ] c · m ≡ n
+
+isProp∣ : isProp (m ∣ n)
+isProp∣ = squash₁
+
+-- Untruncated divisiblility relation
+
+_∣'_ : ℤ → ℤ → Type
+pos 0  ∣' n = 0 ≡ n
+pos (suc m) ∣' n = Σ[ c ∈ ℤ ] c · (pos (suc m)) ≡ n
+(negsuc m)  ∣' n = Σ[ c ∈ ℤ ] c · (negsuc m)    ≡ n
+
+isProp∣' : isProp (m ∣' n)
+isProp∣' {m = pos 0} {n = n} = isSetℤ 0 n
+isProp∣' {m = pos (suc m)} {n = n} p q =
+  Σ≡Prop (λ _ → isSetℤ _ _) (·rCancel (pos (suc m)) _ _ (p .snd ∙ sym (q .snd)) (λ r → snotz (injPos r)))
+isProp∣' {m = negsuc m} {n = n} p q =
+  Σ≡Prop (λ _ → isSetℤ _ _) (·rCancel (negsuc m) _ _ (p .snd ∙ sym (q .snd)) (negsucNotpos _ 0))
+
+∣→∣' : (m n : ℤ) → m ∣ n → m ∣' n
+∣→∣' (pos 0) n ∣ c , p ∣₁   =  sym (·AnnihilR c) ∙ p
+∣→∣' (pos (suc m)) n ∣ p ∣₁ = p
+∣→∣' (negsuc m) n ∣ p ∣₁    = p
+∣→∣' m n (squash₁ p q i)    = isProp∣' (∣→∣' _ _ p) (∣→∣' _ _ q) i
+
+∣'→∣ : (m n : ℤ) → m ∣' n → m ∣ n
+∣'→∣ (pos 0) n p = ∣ 0 , p ∣₁
+∣'→∣ (pos (suc m)) n p = ∣ p ∣₁
+∣'→∣ (negsuc m) n p = ∣ p ∣₁
+
+∣≃∣' : (m n : ℤ) → (m ∣ n) ≃ (m ∣' n)
+∣≃∣' m n = propBiimpl→Equiv isProp∣ isProp∣' (∣→∣' _ _) (∣'→∣ _ _)
+
+-- Properties of divisibility
+
+∣-left : m ∣ (m · k)
+∣-left {k = k} = ∣ k , ·Comm k _ ∣₁
+
+∣-right : m ∣ (k · m)
+∣-right {k = k} =  ∣ k , refl ∣₁
+
+∣-refl : m ≡ n → m ∣ n
+∣-refl p = ∣ 1 ,  ℤ.·IdL _ ∙ p ∣₁
+
+∣-zeroˡ : 0 ∣ m → 0 ≡ m
+∣-zeroˡ = ∣→∣' _ _
+
+∣-zeroʳ : m ∣ 0
+∣-zeroʳ = ∣ 0 , ·AnnihilL _ ∣₁
+
+∣-+ : k ∣ m → k ∣ n → k ∣ (m + n)
+∣-+ =
+  Prop.map2
+    λ {(c₁ , p) (c₂ , q) → (c₁ + c₂ , ·DistL+ c₁ c₂ _ ∙ (λ t → p t + q t))}
+
+∣-trans : k ∣ m → m ∣ n → k ∣ n
+∣-trans =
+  Prop.map2
+    λ {(c₁ , p) (c₂ , q) → (c₂ · c₁ , sym (·Assoc c₂ c₁ _) ∙ cong (c₂ ·_) p ∙ q)}
+
+∣-left· : k ∣ n → k ∣ (n · m)
+∣-left· {k = k} {m = m} p = ∣-trans p (∣-left {k = m})
+
+∣-right· : k ∣ m → k ∣ (n · m)
+∣-right· {k = k} {n = n} p = ∣-trans p (∣-right {k = n})
+
+
+-- Natural numbers back and forth (using abs)
+
+∣→∣ℕ : m ∣ n → abs m ∣ℕ abs n
+∣→∣ℕ {m = m} = Prop.rec isProp∣ℕ (λ (c , h) → ∣ abs c , sym (abs· c m) ∙ cong abs h ∣₁)
+
+private
+  ∣ℕ→∣-helper : (m n : ℤ)
+    → (c : ℕ)(h : c ·ℕ abs m ≡ abs n)
+    → (m ≡ pos (abs m)) ⊎ (m ≡ - pos (abs m))
+    → (n ≡ pos (abs n)) ⊎ (n ≡ - pos (abs n))
+    → Σ[ d ∈ ℤ ] d · m ≡ n
+  ∣ℕ→∣-helper _ _ c _ (inl _) (inl _) .fst = pos c
+  ∣ℕ→∣-helper m n c h (inl p) (inl q) .snd =
+      (λ t → pos c · p t)
+    ∙ cong pos h
+    ∙ sym q
+  ∣ℕ→∣-helper _ _ c _ (inl _) (inr _) .fst = - pos c
+  ∣ℕ→∣-helper m n c h (inl p) (inr q) .snd =
+      (λ t → - pos c · p t)
+    ∙ sym (-DistL· (pos c) (pos (abs m)))
+    ∙ (λ t → - pos·pos c (abs m) (~ t))
+    ∙ cong (-_) (cong pos h)
+    ∙ sym q
+  ∣ℕ→∣-helper _ _ c _ (inr _) (inl _) .fst = - pos c
+  ∣ℕ→∣-helper m n c h (inr p) (inl q) .snd =
+      (λ t → - pos c · p t)
+    ∙ sym (-DistLR· (pos c) (pos (abs m)))
+    ∙ sym (pos·pos c (abs m))
+    ∙ cong pos h
+    ∙ sym q
+  ∣ℕ→∣-helper _ _ c _ (inr _) (inr _) .fst = pos c
+  ∣ℕ→∣-helper m n c h (inr p) (inr q) .snd =
+      (λ t → pos c · p t)
+    ∙ sym (-DistR· (pos c) (pos (abs m)))
+    ∙ (λ t → - pos·pos c (abs m) (~ t))
+    ∙ cong (-_) (cong pos h)
+    ∙ sym q
+
+∣ℕ→∣ : abs m ∣ℕ abs n → m ∣ n
+∣ℕ→∣ = Prop.rec isProp∣ (λ (c , h) → ∣ ∣ℕ→∣-helper _ _ c h (abs→⊎ _ _ refl) (abs→⊎ _ _ refl) ∣₁)
+
+¬∣→¬∣ℕ : ¬ m ∣ n → ¬ abs m ∣ℕ abs n
+¬∣→¬∣ℕ p q = p (∣ℕ→∣ q)
+
+
+-- Inequality for strict divisibility
+
+stDivIneq : ¬ m ≡ 0 → ¬ m ∣ n → k ∣ m → k ∣ n → abs k < abs m
+stDivIneq p q h h' = stDivIneqℕ (¬x≡0→¬abs≡0 p) (¬∣→¬∣ℕ q) (∣→∣ℕ h) (∣→∣ℕ h')
+
+
+-- Exact division
+
+divide : m ∣ n → ℤ
+divide {m = pos 0} _ = 0
+divide {m = pos (suc m)} p = ∣→∣' _ _ p .fst
+divide {m = negsuc m} p = ∣→∣' _ _ p .fst
+
+divideEq : (p : m ∣ n) → divide p · m ≡ n
+divideEq {m = pos 0} = ∣→∣' _ _
+divideEq {m = pos (suc m)} p = ∣→∣' _ _ p .snd
+divideEq {m = negsuc m} p = ∣→∣' _ _ p .snd
+
+
+-- Bézout and Euclidean Domain
+
+record Bézout (m n : ℤ) : Type where
+  constructor bezout
+  field
+    coef₁ : ℤ
+    coef₂ : ℤ
+    gcd   : ℤ
+    identity : coef₁ · m + coef₂ · n ≡ gcd
+    isCD  : (gcd ∣ m) × (gcd ∣ n)
+
+open Bézout
+
+Bézout0 : (n : ℤ) → Bézout 0 n
+Bézout0 n .coef₁ = 0
+Bézout0 n .coef₂ = 1
+Bézout0 n .gcd   = n
+Bézout0 n .identity = ℤ.+IdL _ ∙ ℤ.·IdL n
+Bézout0 n .isCD  = ∣-zeroʳ , ∣-refl refl
+
+bézoutReduction : (m d r : ℤ) → Bézout r m → Bézout m (d · m + r)
+bézoutReduction m d r b .coef₁ = - b .coef₁ · d + b .coef₂
+bézoutReduction m d r b .coef₂ = b .coef₁
+bézoutReduction m d r b .gcd   = b .gcd
+bézoutReduction m d r b .identity =
+   solve! ℤCommRing ∙ b .identity
+bézoutReduction m d r b .isCD .fst = b .isCD .snd
+bézoutReduction m d r b .isCD .snd = ∣-+ (∣-right· {n = d} (b .isCD .snd)) (b .isCD .fst)
+
+-- Properties of Bézout identity
+
+module _
+  (b : Bézout m n) where
+
+  private
+    g = b .gcd
+
+  gcdIsGCD : k ∣ m → k ∣ n → k ∣ g
+  gcdIsGCD {k = k} p q =
+    subst (k ∣_) (b .identity) (∣-+ (∣-right· {n = b .coef₁} p) (∣-right· {n = b .coef₂} q))
+
+  gcd≡0 : g ≡ 0 → (m ≡ 0) × (n ≡ 0)
+  gcd≡0 p .fst = sym (∣-zeroˡ (subst (λ a → a ∣ _) p (b .isCD .fst)))
+  gcd≡0 p .snd = sym (∣-zeroˡ (subst (λ a → a ∣ _) p (b .isCD .snd)))
+
+  ¬m≡0→¬gcd≡0 : ¬ m ≡ 0 → ¬ g ≡ 0
+  ¬m≡0→¬gcd≡0 p q = p (gcd≡0 q .fst)
+
+  div₁ div₂ : ℤ
+  div₁ = divide (b .isCD .fst)
+  div₂ = divide (b .isCD .snd)
+
+  div·-helper : g · (div₁ · n) ≡ g · (div₂ · m)
+  div·-helper =
+      ·Assoc g div₁ n
+    ∙ (λ i → ·Comm g div₁ i · n)
+    ∙ (λ i → divideEq (b .isCD .fst) i · n)
+    ∙ ·Comm m n
+    ∙ (λ i → divideEq (b .isCD .snd) (~ i) · m)
+    ∙ (λ i → ·Comm div₂ g i · m)
+    ∙ sym (·Assoc g div₂ m)
+
+  div·-g≠0 : ¬ g ≡ 0 → div₁ · n ≡ div₂ · m
+  div·-g≠0 p = ·lCancel _ _ _ div·-helper p
+
+  div·-g≡0 : g ≡ 0 → div₁ · n ≡ div₂ · m
+  div·-g≡0 p =
+      (λ i → div₁ · gcd≡0 p .snd i)
+    ∙ ·AnnihilR div₁
+    ∙ sym (·AnnihilR div₂)
+    ∙ λ i → div₂ · gcd≡0 p .fst (~ i)
+
+  div·-case : Dec (g ≡ 0) → div₁ · n ≡ div₂ · m
+  div·-case (yes p) = div·-g≡0  p
+  div·-case (no ¬p) = div·-g≠0 ¬p
+
+  div· : div₁ · n ≡ div₂ · m
+  div· = div·-case (discreteℤ g 0)
+
+  div·- : - div₂ · m + div₁ · n ≡ 0
+  div·- =  (λ i → -DistL· div₂ m (~ i) + div₁ · n)
+          ∙ subst (λ a → - a + div₁ · n ≡ 0) div· (-Cancel' (div₁ · n))
+
+-- Quotient and Remainder
+
+record QuotRem (m n : ℤ) : Type where
+  constructor quotrem
+  field
+    div : ℤ
+    rem : ℤ
+    quotEq : n ≡ div · m + rem
+    normIneq : (rem ≡ 0) ⊎ ((¬ rem ≡ 0) × (abs rem < abs m))
+
+open QuotRem
+
+-- Using remainder to decide divisibility
+
+module _
+  (m n : ℤ)(qr : QuotRem m n) where
+
+  rem≡0→m∣n : qr .rem ≡ 0 → m ∣ n
+  rem≡0→m∣n p = ∣ qr .div ,  sym (ℤ.+IdR _) ∙∙ cong (qr .div · m +_) (sym p) ∙∙ sym (qr .quotEq) ∣₁
+
+  m∣n→rem≡0 : m ∣ n → qr .rem ≡ 0
+  m∣n→rem≡0 p =
+    case qr .normIneq
+    return _ of λ
+    { (inl q) → q
+    ; (inr q) →
+        let ∣+  = ∣-+ p (∣-right {m = m} {k = - qr .div})
+            m∣r = subst {x = n + - qr .div · m} {y = qr .rem}
+                (m ∣_) (cong (_+ _) (qr .quotEq) ∙ solve! ℤCommRing) ∣+
+            m≤r = m∣n→m≤n (¬x≡0→¬abs≡0 (q .fst)) (∣→∣ℕ m∣r)
+        in  Empty.rec (<-asym (q .snd) m≤r) }
+
+  m∣n→rem≡0' : (p : m ∣ n) → qr .normIneq ≡ inl (m∣n→rem≡0 p)
+  m∣n→rem≡0' p =
+    case (qr .normIneq)
+    return (λ x → x ≡ inl (m∣n→rem≡0 p)) of λ
+    { (inl q) → cong inl (isSet→SquareP (λ i j → isSetℤ) q (m∣n→rem≡0 p) refl refl)
+    ; (inr q) → Empty.rec (q .fst (m∣n→rem≡0 p)) }
+
+  rem≢0→m∤n : ¬ qr .rem ≡ 0 → ¬ m ∣ n
+  rem≢0→m∤n p q = p (m∣n→rem≡0 q)
+
+-- The Euclidean Algorithm
+module _
+  (decEq0  : (n : ℤ) → Dec (n ≡ 0))
+  (quotRem : (m n : ℤ)(¬z : ¬ m ≡ 0) → QuotRem m n) where
+
+  euclidStep : (norm : ℕ)
+    → (m n : ℤ)(h : abs m < norm)
+    → (b : QuotRem m n)
+    → Bézout m n
+  euclidStep 0 _ _ h _ = Empty.rec (¬-<-zero h)
+  euclidStep (suc N) m n h (quotrem div rem quotEq (inl p)) =
+    let q = subst (λ r → n ≡ div · m + r) p quotEq
+    in  bezout 1 0 m (
+      1 · m + 0 · n ≡⟨ cong (1 · m +_) (·AnnihilL n) ⟩
+      1 · m + 0     ≡⟨ ℤ.+IdR (1 · m) ⟩
+      1 · m         ≡⟨ ℤ.·IdL m ⟩
+      m             ∎ )
+      (∣-refl refl , subst (λ k → m ∣ k) (sym q) (subst (m ∣_) (sym (ℤ.+IdR (div · m))) (∣-right {k = div})) )
+  euclidStep (suc N) m n h (quotrem div rem quotEq (inr p)) =
+    let b = euclidStep N rem m (<≤-trans (p .snd) (pred-≤-pred h)) (quotRem _ _ (p .fst))
+    in  subst (λ x → Bézout m x) (sym quotEq) (bézoutReduction _ div _ b)
+
+  private
+    euclid-helper : (m n : ℤ)(dec : Dec (m ≡ 0)) → Bézout m n
+    euclid-helper m n (yes z) = subst (λ x → Bézout x n) (sym z) (Bézout0 n)
+    euclid-helper m n (no ¬z) = euclidStep (suc (abs m)) m n ≤-refl (quotRem m n ¬z)
+
+  euclid : (m n : ℤ) → Bézout m n
+  euclid m n = euclid-helper m n (decEq0 _)
+
+  -- Euclid algorithm when divisibility holds
+  euclid∣ : (m n : ℤ) → ¬ m ≡ 0 → m ∣ n → (euclid m n .coef₁ ≡ 1) × (euclid m n .coef₂ ≡ 0)
+  euclid∣ _ _ = euclid∣-helper _ _ (decEq0 _)
+    where
+    euclid∣-helper : (m n : ℤ)(dec : Dec (m ≡ 0)) → ¬ m ≡ 0 → m ∣ n
+      → (euclid-helper m n dec .coef₁ ≡ 1) × (euclid-helper m n dec .coef₂ ≡ 0)
+    euclid∣-helper _ _ (yes z) q = Empty.rec (q z)
+    euclid∣-helper m n (no ¬z) _ q =
+      let qr = quotRem m n ¬z
+          path : qr ≡ quotrem _ _ _ _
+          path t = record qr { normIneq = m∣n→rem≡0' _ _ qr q t }
+      in  (λ t → euclidStep (suc (abs m)) m n ≤-refl (path t) .coef₁) ,
+          (λ t → euclidStep (suc (abs m)) m n ≤-refl (path t) .coef₂)
+
+
+-- The ring ℤ is an Euclidean domain
+
+private
+  dec-helper : {ℓ ℓ' : Level}{A : Type ℓ}{B : Type ℓ'} → Dec A → B → A ⊎ ((¬ A) × B)
+  dec-helper (yes p) _ = inl p
+  dec-helper (no ¬p) b = inr (¬p , b)
+
+quotRemPosPos : (m n : ℕ)(¬z : ¬ pos m ≡ 0) → QuotRem (pos m) (pos n)
+quotRemPosPos m n _ .div = pos (quotient  n / m)
+quotRemPosPos m n _ .rem = pos (remainder n / m)
+quotRemPosPos m n _ .quotEq =
+    (λ t → pos (≡remainder+quotient m n (~ t)))
+  ∙ pos+ (remainder n / m) (m ·ℕ (quotient n / m))
+  ∙ +Comm (pos (remainder n / m)) (pos (m ·ℕ (quotient n / m)))
+  ∙ (λ t → pos·pos m (quotient n / m) t + pos (remainder n / m))
+  ∙ (λ t → ·Comm (pos m) (pos (quotient n / m)) t + pos (remainder n / m))
+quotRemPosPos 0       n ¬z .normIneq = Empty.rec (¬z refl)
+quotRemPosPos (suc m) n ¬z .normIneq = dec-helper (discreteℤ _ 0) (mod< m n)
+
+quotRemNegPos : (m n : ℕ)(¬z : ¬ - pos m ≡ 0) → QuotRem (- pos m) (pos n)
+quotRemNegPos m n ¬z .div = - (quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .div)
+quotRemNegPos m n ¬z .rem = quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .rem
+quotRemNegPos m n ¬z .quotEq =
+    quotRemPosPos m n (λ p → ¬z (λ t → - p t)) .quotEq
+  ∙ (λ t → -DistLR· (pos (quotient n / m)) (pos m) t + (pos (remainder n / m)))
+quotRemNegPos 0       n ¬z .normIneq = Empty.rec (¬z refl)
+quotRemNegPos (suc m) n ¬z .normIneq = quotRemPosPos (suc m) n (λ p → ¬z (λ t → - p t)) .normIneq
+
+private
+  quotRemPos-helper : (m : ℤ)(k n : ℕ)(¬z : ¬ m ≡ 0) → (m ≡ pos k) ⊎ (m ≡ - pos k) → QuotRem m (pos n)
+  quotRemPos-helper m k n ¬z (inl p) =
+    subst (λ l → QuotRem l (pos n)) (sym p) (quotRemPosPos k n (λ r → ¬z (p ∙ r)))
+  quotRemPos-helper m k n ¬z (inr p) =
+    subst (λ l → QuotRem l (pos n)) (sym p) (quotRemNegPos k n (λ r → ¬z (p ∙ r)))
+
+quotRemPos : (m : ℤ)(n : ℕ)(¬z : ¬ m ≡ 0) → QuotRem m (pos n)
+quotRemPos m n ¬z = quotRemPos-helper m (abs m) n ¬z (abs→⊎ _ _ refl)
+
+private
+  sum-helper : (m r : ℤ)
+    → (r ≡ 0)   ⊎ ((¬ r ≡ 0)   × (abs r < abs m))
+    → (- r ≡ 0) ⊎ ((¬ - r ≡ 0) × (abs (- r) < abs m))
+  sum-helper m r (inl p) = inl (λ t → - p t)
+  sum-helper m r (inr p) =
+    inr ((λ q → p .fst (sym (-Involutive r) ∙ (λ t → - q t)))
+      , subst (λ k → k < abs m) (sym (abs- r)) (p .snd))
+
+quotRemNeg : (m : ℤ)(n : ℕ)(¬z : ¬ m ≡ 0) → QuotRem m (- pos n)
+quotRemNeg m n ¬z .div = - (quotRemPos m n ¬z .div)
+quotRemNeg m n ¬z .rem = - (quotRemPos m n ¬z .rem)
+quotRemNeg m n ¬z .quotEq =
+    (λ t → - quotRemPos m n ¬z .quotEq t)
+  ∙ -Dist+ (quotRemPos m n ¬z .div · m) (quotRemPos m n ¬z .rem)
+  ∙ (λ t → -DistL· (quotRemPos m n ¬z .div) m t + - quotRemPos m n ¬z .rem)
+quotRemNeg m n ¬z .normIneq = sum-helper m _ (quotRemPos m n ¬z .normIneq)
+
+private
+  quotRem-helper : (m n : ℤ)(k : ℕ)(¬z : ¬ m ≡ 0) → (n ≡ pos k) ⊎ (n ≡ - pos k) → QuotRem m n
+  quotRem-helper m n k ¬z (inl p) = subst (λ l → QuotRem m l) (sym p) (quotRemPos m k ¬z)
+  quotRem-helper m n k ¬z (inr p) = subst (λ l → QuotRem m l) (sym p) (quotRemNeg m k ¬z)
+
+
+-- The quotient-remainder Theorem and the Bézout identity
+
+quotRem : (m n : ℤ)(¬z : ¬ m ≡ 0) → QuotRem m n
+quotRem m n ¬z = quotRem-helper m n (abs n) ¬z (abs→⊎ _ _ refl)
+
+bézout : (m n : ℤ) → Bézout m n
+bézout = euclid (λ m → discreteℤ m 0) quotRem
+
+bézout∣ : (m n : ℤ) → ¬ m ≡ 0 → m ∣ n → (bézout m n .coef₁ ≡ 1) × (bézout m n .coef₂ ≡ 0)
+bézout∣ = euclid∣ (λ m → discreteℤ m 0) quotRem
+
+
+-- Divisibility is decidable
+dec∣ : (m n : ℤ) → Dec (m ∣ n)
+dec∣ m n =
+  case discreteℤ m 0
+  return (λ _ → Dec (m ∣ n)) of λ
+  { (yes p) →
+      case discreteℤ n 0
+      return (λ _ → Dec (m ∣ n)) of λ
+      { (yes p) → yes (subst (m ∣_) (sym p) ∣-zeroʳ)
+      ; (no ¬p) → no  (λ r → ¬p (sym (∣-zeroˡ (subst (_∣ n) p r)))) }
+  ; (no ¬p) →
+      let qr = quotRem m n ¬p in
+      case discreteℤ (qr .rem) 0
+      return (λ _ → Dec (m ∣ n)) of λ
+      { (yes p) → yes (rem≡0→m∣n _ _ qr  p)
+      ; (no ¬p) → no  (rem≢0→m∤n _ _ qr ¬p) }}
diff --git a/Cubical/Data/Fast/Int/IsEven.agda b/Cubical/Data/Fast/Int/IsEven.agda
new file mode 100644
index 0000000000..eac8938dad
--- /dev/null
+++ b/Cubical/Data/Fast/Int/IsEven.agda
@@ -0,0 +1,135 @@
+module Cubical.Data.Fast.Int.IsEven where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Bool
+open import Cubical.Data.Nat
+  using (ℕ ; zero ;  suc ; +-zero ; +-suc ; injSuc ; +-comm ; snotz ; znots ; ·-distribˡ)
+  renaming
+  (_+_    to _+ℕ_ ;
+   _·_    to _·ℕ_ ;
+   isEven to isEvenℕ ;
+   isOdd  to isOddℕ)
+import Cubical.Data.Nat.IsEven as ℕeven
+
+open import Cubical.Data.Fast.Int.Base as ℤ
+open import Cubical.Data.Fast.Int.Properties
+open import Cubical.Data.Sum
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Instances.Bool
+open import Cubical.Algebra.Group.Instances.Fast.Int
+
+open GroupStr (snd BoolGroup) using ()
+  renaming ( _·_ to _+Bool_ )
+
+-----------------------------------------------------------------------------
+-- Lemma over ℤ
+
+2negsuc : (k : ℕ) → 2 · negsuc k ≡ negsuc (1 +ℕ 2 ·ℕ k)
+2negsuc k = cong negsuc (+-suc k (k +ℕ zero))
+
+1+2kNegsuc : (k : ℕ) → 1 + 2 · negsuc k ≡ negsuc (2 ·ℕ k)
+1+2kNegsuc k = cong (λ X → 1 + X)
+                    ( 2negsuc k
+                    ∙ cong negsuc (+-comm 1 (2 ·ℕ k))
+                    ∙ negsuc+ (2 ·ℕ k) 1
+                    ∙ +Comm (negsuc (2 ·ℕ k)) (- 1))
+               ∙ sym (pos0+ (negsuc (2 ·ℕ k)))
+
+1+2kPos : (k : ℕ) → pos (1 +ℕ 2 ·ℕ k) ≡ 1 + 2 · (pos k)
+1+2kPos k = refl
+
+-- isEven → 2k / isOdd → 1 + 2k
+isEvenTrue : (a : ℤ) → (isEven a ≡ true) → Σ[ m ∈ ℤ ] a ≡ (2 · m)
+isEvenTrue (pos n) p = (pos k) , cong pos pp
+  where
+  k = fst (ℕeven.isEvenTrue n p)
+  pp = snd (ℕeven.isEvenTrue n p)
+isEvenTrue (negsuc n) p = (negsuc k) , cong negsuc pp ∙ sym (2negsuc k)
+  where
+  k = fst (ℕeven.isOddTrue n p)
+  pp = snd (ℕeven.isOddTrue n p)
+
+isEvenFalse : (a : ℤ) → (isEven a ≡ false) → Σ[ m ∈ ℤ ] a ≡ 1 + (2 · m)
+isEvenFalse (pos n) p = (pos k) , (cong pos pp)
+  where
+  k = fst (ℕeven.isEvenFalse n p)
+  pp = snd (ℕeven.isEvenFalse n p)
+isEvenFalse (negsuc n) p = (negsuc k) , (cong negsuc pp ∙ sym (1+2kNegsuc k))
+  where
+  k = fst (ℕeven.isOddFalse n p)
+  pp = snd (ℕeven.isOddFalse n p)
+
+
+-- 2k → isEven / 1 + 2k → isOdd
+trueIsEven : (a : ℤ)  → Σ[ m ∈ ℤ ] a ≡ (2 · m) → (isEven a ≡ true)
+trueIsEven (pos n) (pos m , p) = ℕeven.trueIsEven n (m , injPos p)
+trueIsEven (pos n) (negsuc m , p) = ⊥.rec (posNotnegsuc n (1 +ℕ 2 ·ℕ m) (p ∙ 2negsuc m))
+trueIsEven (negsuc n) (pos m , p) = ⊥.rec (negsucNotpos n (2 ·ℕ m) p)
+trueIsEven (negsuc n) (negsuc m , p) = ℕeven.¬IsEvenFalse n (ℕeven.falseIsEven n
+                                       (m , (injNegsuc (p ∙ 2negsuc m))))
+
+falseIsEven : (a : ℤ) → Σ[ m ∈ ℤ ] a ≡ 1 + (2 · m) → isEven a ≡ false
+falseIsEven (pos n) (pos m , p) = ℕeven.falseIsEven n (m , injPos p)
+falseIsEven (pos n) (negsuc m , p) = ⊥.rec (posNotnegsuc n (2 ·ℕ m) (p ∙ 1+2kNegsuc m))
+falseIsEven (negsuc n) (pos m , p) = ⊥.rec (negsucNotpos n (1 +ℕ 2 ·ℕ m) (p ∙ sym (1+2kPos m)))
+falseIsEven (negsuc n) (negsuc m , p) = ℕeven.¬IsEvenTrue n (ℕeven.trueIsEven n (m , (injNegsuc (p ∙ 1+2kNegsuc m ))))
+
+
+-- Value of isEven (x + y)  depending on IsEven x, IsEven y
+isOddIsOdd→IsEven : (x y : ℤ) → isEven x ≡ false → isEven y ≡ false → isEven (x + y) ≡ true
+isOddIsOdd→IsEven x y px py = trueIsEven (x + y) ((1 + k + l) , cong₂ _+_ qk ql ∙ sym helper)
+  where
+  k  = fst (isEvenFalse x px)
+  qk = snd (isEvenFalse x px)
+  l  = fst (isEvenFalse y py)
+  ql = snd (isEvenFalse y py)
+  helper : 2 · ((1 + k) + l) ≡ (1 + 2 · k) + (1 + 2 · l)
+  helper = 2 · ((1 + k) + l)         ≡⟨ ·DistR+ 2 (1 + k) l ⟩
+           2 · (1 + k) + 2 · l       ≡⟨ cong (_+ 2 · l) (·DistR+ 2 1 k) ⟩
+           (1 + 1 + 2 · k) + 2 · l   ≡⟨ cong (_+ 2 · l) (sym (+Assoc 1 1 (2 · k))) ⟩
+           1 + (1 + 2 · k) + 2 · l   ≡⟨ cong (λ r → 1 + r + 2 · l) (+Comm 1 (2 · k)) ⟩
+           1 + (2 · k + 1) + 2 · l   ≡⟨ cong (_+ 2 · l) (+Assoc 1 (2 · k) 1) ⟩
+           ((1 + 2 · k) + 1) + 2 · l ≡⟨ sym (+Assoc (1 + 2 · k) 1 (2 · l)) ⟩
+           (1 + 2 · k) + (1 + 2 · l) ∎
+
+isOddIsEven→IsOdd : (x y : ℤ) → isEven x ≡ false → isEven y ≡ true → isEven (x + y) ≡ false
+isOddIsEven→IsOdd x y px py = falseIsEven (x + y) ((k + l) , ( cong₂ _+_ qk ql ∙ helper))
+  where
+  k  = fst (isEvenFalse x px)
+  qk = snd (isEvenFalse x px)
+  l  = fst (isEvenTrue y py)
+  ql = snd (isEvenTrue y py)
+  helper : _
+  helper = (1 + 2 · k) + 2 · l ≡⟨ sym (+Assoc 1 (2 · k) (2 · l)) ⟩
+           1 + (2 · k + 2 · l) ≡⟨ cong (1 +_) ( sym (·DistR+ 2 k l)) ⟩
+           1 + 2 · (k + l)     ∎
+
+isEvenIsOdd→IsOdd : (x y : ℤ) → isEven x ≡ true → isEven y ≡ false → isEven (x + y) ≡ false
+isEvenIsOdd→IsOdd x y px py = cong isEven (+Comm x y) ∙ isOddIsEven→IsOdd y x py px
+
+isEvenIsEven→IsEven : (x y : ℤ) → isEven x ≡ true → isEven y ≡ true → isEven (x + y) ≡ true
+isEvenIsEven→IsEven x y px py = trueIsEven (x + y) ((k + l) , cong₂ _+_ qk ql ∙ sym (·DistR+ 2 k l))
+  where
+  k =  fst (isEvenTrue x px)
+  qk = snd (isEvenTrue x px)
+  l = fst (isEvenTrue y py)
+  ql = snd (isEvenTrue y py)
+
+
+-- Proof that isEven is morphism
+isEven-pres+ : (x y : ℤ) → isEven (x + y) ≡ isEven x +Bool isEven y
+isEven-pres+ x y with (dichotomyBoolSym (isEven x)) | dichotomyBoolSym (isEven y)
+... | inl xf | inl yf = isOddIsOdd→IsEven x y xf yf ∙ sym (cong₂ _+Bool_ xf yf)
+... | inl xf | inr yt = isOddIsEven→IsOdd x y xf yt ∙ sym (cong₂ _+Bool_ xf yt)
+... | inr xt | inl yf = isEvenIsOdd→IsOdd x y xt yf ∙ sym (cong₂ _+Bool_ xt yf)
+... | inr xt | inr yt = isEvenIsEven→IsEven x y xt yt ∙ sym (cong₂ _+Bool_ xt yt)
+
+isEven-GroupMorphism : IsGroupHom (snd ℤGroup) isEven (snd BoolGroup)
+isEven-GroupMorphism = makeIsGroupHom isEven-pres+
diff --git a/Cubical/Data/Fast/Int/Order.agda b/Cubical/Data/Fast/Int/Order.agda
new file mode 100644
index 0000000000..5b360fa490
--- /dev/null
+++ b/Cubical/Data/Fast/Int/Order.agda
@@ -0,0 +1,741 @@
+{- Order as an Indexed Data Type, as done in Agda stdlib and 1Lab -}
+module Cubical.Data.Fast.Int.Order where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Bool hiding (_≟_ ; _≤_ ; _≥_ ; isProp≤)
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum
+
+open import Cubical.Data.Nat as ℕ
+open import Cubical.Data.Nat.Order as ℕ using ()
+open import Cubical.Data.Nat.Order.Inductive as ℕ
+open import Cubical.Data.Fast.Int as ℤ
+
+private
+  variable
+    m n o s : ℤ
+    k l : ℕ
+
+infix 4 _≤_ _<_ _≥_ _>_
+
+data _≤_ : ℤ → ℤ → Type where
+  pos≤pos       : ∀ {x y} → x ℕ.≤ᵗ y → pos x    ≤ pos y
+  negsuc≤negsuc : ∀ {x y} → x ℕ.≥ᵗ y → negsuc x ≤ negsuc y
+  negsuc≤pos    : ∀ {x y}            → negsuc x ≤ pos y
+
+data _<_ : ℤ → ℤ → Type where
+  pos<pos       : ∀ {x y} → x ℕ.<ᵗ y → pos x    < pos y
+  negsuc<negsuc : ∀ {x y} → x ℕ.>ᵗ y → negsuc x < negsuc y
+  negsuc<pos    : ∀ {x y}            → negsuc x < pos y
+
+_≥_ _>_ : ℤ → ℤ → Type
+_≥_ = flip _≤_
+_>_ = flip _<_
+
+¬pos≤negsuc : ∀ {x y} → ¬ pos x ≤ negsuc y
+¬pos≤negsuc ()
+
+¬pos<negsuc : ∀ {x y} → ¬ pos x < negsuc y
+¬pos<negsuc ()
+
+¬≤ℕ→¬pos≤pos : ∀ {x y} → ¬ (x ℕ.≤ᵗ y) → ¬ pos x ≤ pos y
+¬≤ℕ→¬pos≤pos ¬p (pos≤pos p) = ¬p p
+
+¬<ℕ→¬pos<pos : ∀ {x y} → ¬ (x ℕ.<ᵗ y) → ¬ pos x < pos y
+¬<ℕ→¬pos<pos ¬p (pos<pos p) = ¬p p
+
+¬≥ℕ→¬negsuc≤negsuc : ∀ {x y} → ¬ (x ℕ.≥ᵗ y) → ¬ negsuc x ≤ negsuc y
+¬≥ℕ→¬negsuc≤negsuc ¬p (negsuc≤negsuc p) = ¬p p
+
+¬>ℕ→¬negsuc<negsuc : ∀ {x y} → ¬ (x ℕ.>ᵗ y) → ¬ negsuc x < negsuc y
+¬>ℕ→¬negsuc<negsuc ¬p (negsuc<negsuc p) = ¬p p
+
+{-# DISPLAY negsuc≤negsuc {x} {y} _ = negsuc x ≤ negsuc y #-}
+{-# DISPLAY pos≤pos       {x} {y} _ =    pos x ≤ pos y #-}
+{-# DISPLAY negsuc≤pos    {x} {y}   = negsuc x ≤ pos y #-}
+
+{-# DISPLAY negsuc<negsuc {x} {y} _ = negsuc x < negsuc y #-}
+{-# DISPLAY pos<pos       {x} {y} _ =    pos x < pos y #-}
+{-# DISPLAY negsuc<pos    {x} {y}   = negsuc x < pos y #-}
+
+{-# DISPLAY ¬≤ℕ→¬pos≤pos       {x} {y} _ = ¬ pos x    ≤ pos y    #-}
+{-# DISPLAY ¬≥ℕ→¬negsuc≤negsuc {x} {y} _ = ¬ negsuc x ≤ negsuc y #-}
+{-# DISPLAY ¬pos≤negsuc        {x} {y}   = ¬    pos x ≤ negsuc y #-}
+
+{-# DISPLAY ¬<ℕ→¬pos<pos       {x} {y} _ = ¬ pos x    < pos y    #-}
+{-# DISPLAY ¬>ℕ→¬negsuc<negsuc {x} {y} _ = ¬ negsuc x < negsuc y #-}
+{-# DISPLAY ¬pos<negsuc        {x} {y}   = ¬    pos x < negsuc y #-}
+
+isProp≤ : isProp (m ≤ n)
+isProp≤ (pos≤pos p)       (pos≤pos q)       = cong pos≤pos (isPropBool→Type p q)
+isProp≤  negsuc≤pos        negsuc≤pos       = refl
+isProp≤ (negsuc≤negsuc p) (negsuc≤negsuc q) = cong negsuc≤negsuc (isPropBool→Type p q)
+
+isProp< : isProp (m < n)
+isProp< (pos<pos p)       (pos<pos q)       = cong pos<pos (isPropBool→Type p q)
+isProp<  negsuc<pos        negsuc<pos       = refl
+isProp< (negsuc<negsuc p) (negsuc<negsuc q) = cong negsuc<negsuc (isPropBool→Type p q)
+
+_≤?_ ≤Dec : ∀ m n → Dec (m ≤ n)
+pos m    ≤? pos n    = mapDec pos≤pos ¬≤ℕ→¬pos≤pos DecBool→Type
+pos m    ≤? negsuc n = no ¬pos≤negsuc
+negsuc m ≤? pos n    = yes negsuc≤pos
+negsuc m ≤? negsuc n = mapDec negsuc≤negsuc ¬≥ℕ→¬negsuc≤negsuc DecBool→Type
+
+≤Dec = _≤?_
+
+_<?_ <Dec : ∀ m n → Dec (m < n)
+pos m    <? pos n    = mapDec pos<pos ¬<ℕ→¬pos<pos DecBool→Type
+pos m    <? negsuc n = no ¬pos<negsuc
+negsuc m <? pos n    = yes negsuc<pos
+negsuc m <? negsuc n = mapDec negsuc<negsuc ¬>ℕ→¬negsuc<negsuc DecBool→Type
+
+<Dec = _<?_
+
+≤Stable : ∀ m n → Stable (m ≤ n)
+≤Stable m n = Dec→Stable (m ≤? n)
+
+<Stable : ∀ m n → Stable (m < n)
+<Stable m n = Dec→Stable (m <? n)
+
+-- auxilary functions to speed up proofs, relying on the decidability of order
+
+recompute< : (m < n) → (m < n)
+recompute< p = decRec (idfun _) (λ _ → p) (_ <? _)
+
+recompute≤ : (m ≤ n) → (m ≤ n)
+recompute≤ p = decRec (idfun _) (λ _ → p) (_ ≤? _)
+
+recompute¬< : ¬ (m < n) → ¬ (m < n)
+recompute¬< p = decRec (λ _ → p) (idfun _) (_ <? _)
+
+recompute¬≤ : ¬ (m ≤ n) → ¬ (m ≤ n)
+recompute¬≤ p = decRec (λ _ → p) (idfun _) (_ ≤? _)
+
+-- properties of _<_ and _≤_
+
+zero-≤pos : 0 ≤ pos l
+zero-≤pos = pos≤pos tt
+
+zero-<possuc : 0 < pos (suc l)
+zero-<possuc = pos<pos tt
+
+negsuc≤-zero : negsuc k ≤ 0
+negsuc≤-zero = negsuc≤pos
+
+negsuc<-zero : negsuc k < 0
+negsuc<-zero = negsuc<pos
+
+¬-pos<-zero : ¬ (pos k) < 0
+¬-pos<-zero (pos<pos ())
+
+suc-≤-suc : m ≤ n → sucℤ m ≤ sucℤ n
+suc-≤-suc {pos m}          {pos n}          (pos≤pos p)       = pos≤pos p
+suc-≤-suc {negsuc zero}    {pos n}           negsuc≤pos       = pos≤pos tt
+suc-≤-suc {negsuc (suc m)} {pos n}           negsuc≤pos       = negsuc≤pos
+suc-≤-suc {negsuc zero}    {negsuc zero}    (negsuc≤negsuc p) = pos≤pos tt
+suc-≤-suc {negsuc (suc m)} {negsuc zero}    (negsuc≤negsuc p) = negsuc≤pos
+suc-≤-suc {negsuc (suc m)} {negsuc (suc n)} (negsuc≤negsuc p) = negsuc≤negsuc p
+
+suc-<-suc : m < n → sucℤ m < sucℤ n
+suc-<-suc {pos m}          {pos n}          (pos<pos p)       = pos<pos p
+suc-<-suc {negsuc zero}    {pos n}           negsuc<pos       = pos<pos tt
+suc-<-suc {negsuc (suc m)} {pos n}           negsuc<pos       = negsuc<pos
+suc-<-suc {negsuc (suc m)} {negsuc zero}    (negsuc<negsuc p) = negsuc<pos
+suc-<-suc {negsuc (suc m)} {negsuc (suc n)} (negsuc<negsuc p) = negsuc<negsuc p
+
+pred-≤-pred : sucℤ m ≤ sucℤ n → m ≤ n
+pred-≤-pred {pos m}          {pos n}          (pos≤pos p)       = pos≤pos p
+pred-≤-pred {pos zero}       {negsuc zero}    (pos≤pos ())
+pred-≤-pred {negsuc m}       {pos n}           _                = negsuc≤pos
+pred-≤-pred {negsuc zero}    {negsuc zero}    (pos≤pos p)       = negsuc≤negsuc tt
+pred-≤-pred {negsuc (suc m)} {negsuc zero}     negsuc≤pos       = negsuc≤negsuc tt
+pred-≤-pred {negsuc (suc m)} {negsuc (suc n)} (negsuc≤negsuc p) = negsuc≤negsuc p
+
+pred-<-pred : sucℤ m < sucℤ n → m < n
+pred-<-pred {pos m}          {pos n}          (pos<pos p)       = pos<pos p
+pred-<-pred {pos zero}       {negsuc zero}    (pos<pos ())
+pred-<-pred {negsuc m}       {pos n}           _                = negsuc<pos
+pred-<-pred {negsuc zero}    {negsuc zero}    (pos<pos ())
+pred-<-pred {negsuc (suc m)} {negsuc zero}     negsuc<pos       = negsuc<negsuc tt
+pred-<-pred {negsuc (suc m)} {negsuc (suc n)} (negsuc<negsuc p) = negsuc<negsuc p
+
+predℤ-≤-predℤ : m ≤ n → predℤ m ≤ predℤ n
+predℤ-≤-predℤ {pos zero}    {pos zero}    (pos≤pos p)       = negsuc≤negsuc tt
+predℤ-≤-predℤ {pos zero}    {pos (suc n)} (pos≤pos p)       = negsuc≤pos
+predℤ-≤-predℤ {pos (suc m)} {pos (suc n)} (pos≤pos p)       = pos≤pos p
+predℤ-≤-predℤ {negsuc m}    {pos zero}     negsuc≤pos       = negsuc≤negsuc tt
+predℤ-≤-predℤ {negsuc m}    {pos (suc n)}  negsuc≤pos       = negsuc≤pos
+predℤ-≤-predℤ {negsuc m}    {negsuc n}    (negsuc≤negsuc p) = negsuc≤negsuc p
+
+predℤ-<-predℤ : m < n → predℤ m < predℤ n
+predℤ-<-predℤ {pos zero}    {pos (suc n)} (pos<pos p)       = negsuc<pos
+predℤ-<-predℤ {pos (suc m)} {pos (suc n)} (pos<pos p)       = pos<pos p
+predℤ-<-predℤ {negsuc m}    {pos zero}     negsuc<pos       = negsuc<negsuc tt
+predℤ-<-predℤ {negsuc m}    {pos (suc n)}  negsuc<pos       = negsuc<pos
+predℤ-<-predℤ {negsuc m}    {negsuc n}    (negsuc<negsuc p) = negsuc<negsuc p
+
+pos≤pos→negsuc≥negsuc : pos k ≤ pos l → negsuc k ≥ negsuc l
+pos≤pos→negsuc≥negsuc (pos≤pos p) = negsuc≤negsuc p
+
+pos<pos→negsuc>negsuc : pos k < pos l → negsuc k > negsuc l
+pos<pos→negsuc>negsuc (pos<pos p) = negsuc<negsuc p
+
+negsuc≤negsuc→pos≥pos : negsuc k ≤ negsuc l → pos k ≥ pos l
+negsuc≤negsuc→pos≥pos (negsuc≤negsuc p) = pos≤pos p
+
+negsuc<negsuc→pos>pos : negsuc k < negsuc l → pos k > pos l
+negsuc<negsuc→pos>pos (negsuc<negsuc p) = pos<pos p
+
+pos≤pos→neg≥neg : pos k ≤ pos l → neg k ≥ neg l
+pos≤pos→neg≥neg {zero}  {zero}  (pos≤pos p) = pos≤pos tt
+pos≤pos→neg≥neg {zero}  {suc l} (pos≤pos p) = negsuc≤pos
+pos≤pos→neg≥neg {suc k} {suc l} (pos≤pos p) = negsuc≤negsuc p
+
+pos<pos→neg>neg : pos k < pos l → neg k > neg l
+pos<pos→neg>neg {zero}  {suc l} (pos<pos p) = negsuc<pos
+pos<pos→neg>neg {suc k} {suc l} (pos<pos p) = negsuc<negsuc p
+
+<→suc≤ : m < n → sucℤ m ≤ n
+<→suc≤ {pos m}          {pos n}    (pos<pos p)       = pos≤pos p
+<→suc≤ {negsuc zero}    {pos n}     negsuc<pos       = pos≤pos tt
+<→suc≤ {negsuc (suc m)} {pos n}     negsuc<pos       = negsuc≤pos
+<→suc≤ {negsuc (suc m)} {negsuc n} (negsuc<negsuc p) = negsuc≤negsuc p
+
+suc≤→< : sucℤ m ≤ n → m < n
+suc≤→< {pos m}          {pos n}    (pos≤pos p)       = pos<pos p
+suc≤→< {negsuc m}       {pos n}     _                = negsuc<pos
+suc≤→< {negsuc (suc m)} {negsuc n} (negsuc≤negsuc p) = negsuc<negsuc p
+
+<≃suc≤ : (m < n) ≃ (sucℤ m ≤ n)
+<≃suc≤ = propBiimpl→Equiv isProp< isProp≤ <→suc≤ suc≤→<
+
+<≡suc≤ : (m < n) ≡ (sucℤ m ≤ n)
+<≡suc≤ = ua <≃suc≤
+
+≤→<suc : m ≤ n → m < sucℤ n
+≤→<suc {pos m}    {pos n}          (pos≤pos p)       = pos<pos p
+≤→<suc {negsuc m} {pos n}           negsuc≤pos       = negsuc<pos
+≤→<suc {negsuc m} {negsuc zero}    (negsuc≤negsuc p) = negsuc<pos
+≤→<suc {negsuc m} {negsuc (suc n)} (negsuc≤negsuc p) = negsuc<negsuc p
+
+<suc→≤ : m < sucℤ n → m ≤ n
+<suc→≤ {pos m}          {pos n}          (pos<pos p)       = pos≤pos p
+<suc→≤ {negsuc m}       {pos n}           negsuc<pos       = negsuc≤pos
+<suc→≤ {pos m}          {negsuc zero}    (pos<pos ())
+<suc→≤ {negsuc m}       {negsuc zero}     negsuc<pos       = negsuc≤negsuc tt
+<suc→≤ {negsuc (suc m)} {negsuc (suc n)} (negsuc<negsuc p) = negsuc≤negsuc p
+
+≤≃<suc : (m ≤ n) ≃ (m < sucℤ n)
+≤≃<suc = propBiimpl→Equiv isProp≤ isProp< ≤→<suc <suc→≤
+
+≤≡<suc : (m ≤ n) ≡ (m < sucℤ n)
+≤≡<suc = ua ≤≃<suc
+
+≤-+o : m ≤ n → m ℤ.+ o ≤ n ℤ.+ o
+≤-+o = recompute≤ ∘ proof _ _ _ where
+  proof : ∀ m n o → m ≤ n → m ℤ.+ o ≤ n ℤ.+ o
+  proof m n (pos zero)       = subst2 _≤_ (sym (ℤ.+IdR m)) (sym (ℤ.+IdR n))
+  proof m n (pos (suc k))    = subst2 _≤_
+    (+sucℤ m _) (+sucℤ n _) ∘ suc-≤-suc ∘ proof m n (pos k)
+  proof m n (negsuc zero)    = subst2 _≤_ (+negsuc0 m) (+negsuc0 n) ∘ predℤ-≤-predℤ
+  proof m n (negsuc (suc k)) = subst2 _≤_
+    (+predℤ m _) (+predℤ n _) ∘ predℤ-≤-predℤ ∘ proof m n (negsuc k)
+
+<-+o : m < n → (m ℤ.+ o) < (n ℤ.+ o)
+<-+o {m} {n} {o} = recompute< ∘ suc≤→< ∘ subst (_≤ _) (sym (sucℤ+ m o)) ∘ ≤-+o ∘ <→suc≤
+
+≤SumRightPos : n ≤ pos k ℤ.+ n
+≤SumRightPos {n} {k} = recompute≤ $ subst (_≤ pos k ℤ.+ n) (ℤ.+IdL n) (≤-+o {o = n} zero-≤pos)
+
+<SumRightPosSuc : n < pos (suc k) ℤ.+ n
+<SumRightPosSuc {n} {k} = recompute< $ subst (_< pos (suc k) ℤ.+ n) (ℤ.+IdL n) (<-+o {o = n} zero-<possuc)
+
+≤-o+ : m ≤ n → o ℤ.+ m ≤ o ℤ.+ n
+≤-o+ {m} {n} {o} = recompute≤ ∘ subst2 (_≤_) (+Comm m o) (+Comm n o) ∘ ≤-+o
+
+<-o+ : m < n → (o ℤ.+ m) < (o ℤ.+ n)
+<-o+ {m} {n} {o} = recompute< ∘ subst2 (_<_) (+Comm m o) (+Comm n o) ∘ <-+o
+
+≤SumLeftPos : n ≤ n ℤ.+ pos k
+≤SumLeftPos {n} {k} = recompute≤ $ subst (n ≤_) (+Comm (pos k) n) ≤SumRightPos
+
+<SumLeftPosSuc : n < n ℤ.+ pos (suc k)
+<SumLeftPosSuc {n} {k} = recompute< $ subst (n <_) (+Comm (pos (suc k)) n) <SumRightPosSuc
+
+isRefl≤ : m ≤ m
+isRefl≤ = recompute≤ $ proof _ where
+  proof : ∀ m → m ≤ m
+  proof (pos zero)       = pos≤pos tt
+  proof (pos (suc n))    = suc-≤-suc (proof (pos n))
+  proof (negsuc zero)    = negsuc≤negsuc tt
+  proof (negsuc (suc n)) = predℤ-≤-predℤ (proof (negsuc n))
+
+≤-suc : m ≤ n → m ≤ sucℤ n
+≤-suc = recompute≤ ∘ proof _ _ where
+  proof : ∀ m n → m ≤ n → m ≤ sucℤ n
+  proof (pos zero)       (pos zero)             (pos≤pos p)       = pos≤pos tt
+  proof (pos zero)       (pos (suc n))          (pos≤pos p)       = pos≤pos tt
+  proof (pos (suc m))    (pos (suc n))          (pos≤pos p)       =
+    suc-≤-suc (proof (pos m) (pos n) (pos≤pos p))
+  proof (negsuc m)       (pos n)                 negsuc≤pos       = negsuc≤pos
+  proof (negsuc zero)    (negsuc zero)          (negsuc≤negsuc p) = negsuc≤pos
+  proof (negsuc (suc m)) (negsuc zero)          (negsuc≤negsuc p) = negsuc≤pos
+  proof (negsuc (suc m)) (negsuc (suc zero))    (negsuc≤negsuc p) = negsuc≤negsuc tt
+  proof (negsuc (suc m)) (negsuc (suc (suc n))) (negsuc≤negsuc p) =
+    predℤ-≤-predℤ (proof (negsuc m) (negsuc (suc n)) (negsuc≤negsuc p))
+
+suc-< : sucℤ m < n → m < n
+suc-< = suc≤→< ∘ pred-≤-pred ∘ ≤-suc ∘ <→suc≤
+
+≤-sucℤ : n ≤ sucℤ n
+≤-sucℤ = ≤-suc isRefl≤
+
+<-sucℤ : n < sucℤ n
+<-sucℤ = ≤→<suc isRefl≤
+
+isTrans≤ : m ≤ n → n ≤ o → m ≤ o
+isTrans≤ = (recompute≤ ∘_) ∘ proof _ _ _ where
+  proof : ∀ m n o → m ≤ n → n ≤ o → m ≤ o
+  proof (pos zero)       (pos zero)       (pos zero)       (pos≤pos p)       (pos≤pos q)       =
+    pos≤pos tt
+  proof (pos zero)       (pos zero)       (pos (suc o))    (pos≤pos p)       (pos≤pos q)       =
+    pos≤pos tt
+  proof (pos zero)       (pos (suc n))    (pos (suc o))    (pos≤pos p)       (pos≤pos q)       =
+    pos≤pos tt
+  proof (pos (suc m))    (pos (suc n))    (pos (suc o))    (pos≤pos p)       (pos≤pos q)       =
+    suc-≤-suc (proof (pos m) (pos n) (pos o) (pos≤pos p) (pos≤pos q))
+  proof (negsuc m)       (pos n)          (pos o)           negsuc≤pos       (pos≤pos q)       =
+    negsuc≤pos
+  proof (negsuc m)       (negsuc n)       (pos o)          (negsuc≤negsuc p)  negsuc≤pos       =
+    negsuc≤pos
+  proof (negsuc zero)    (negsuc zero)    (negsuc zero)    (negsuc≤negsuc p) (negsuc≤negsuc q) =
+    negsuc≤negsuc tt
+  proof (negsuc (suc m)) (negsuc zero)    (negsuc zero)    (negsuc≤negsuc p) (negsuc≤negsuc q) =
+    negsuc≤negsuc tt
+  proof (negsuc (suc m)) (negsuc (suc n)) (negsuc zero)    (negsuc≤negsuc p) (negsuc≤negsuc q) =
+    negsuc≤negsuc tt
+  proof (negsuc (suc m)) (negsuc (suc n)) (negsuc (suc o)) (negsuc≤negsuc p) (negsuc≤negsuc q) =
+    predℤ-≤-predℤ (proof (negsuc m) (negsuc n) (negsuc o) (negsuc≤negsuc p) (negsuc≤negsuc q))
+
+isTrans< : m < n → n < o → m < o
+isTrans< = (recompute< ∘_) ∘ proof _ _ _ where
+  proof : ∀ m n o → m < n → n < o → m < o
+  proof (pos zero)       (pos (suc n))    (pos (suc o))    (pos<pos p)       (pos<pos q)       =
+    pos<pos tt
+  proof (pos (suc m))    (pos (suc n))    (pos (suc o))    (pos<pos p)       (pos<pos q)       =
+    suc-<-suc (proof (pos m) (pos n) (pos o) (pos<pos p) (pos<pos q))
+  proof (negsuc m)       (pos n)          (pos o)           negsuc<pos       (pos<pos q)       =
+    negsuc<pos
+  proof (negsuc m)       (negsuc n)       (pos o)          (negsuc<negsuc p)  negsuc<pos       =
+    negsuc<pos
+  proof (negsuc (suc m)) (negsuc (suc n)) (negsuc zero)    (negsuc<negsuc p) (negsuc<negsuc q) =
+    negsuc<negsuc tt
+  proof (negsuc (suc m)) (negsuc (suc n)) (negsuc (suc o)) (negsuc<negsuc p) (negsuc<negsuc q) =
+    predℤ-<-predℤ (proof (negsuc m) (negsuc n) (negsuc o) (negsuc<negsuc p) (negsuc<negsuc q))
+
+-- this proof will not normalize quickly when m and n are the same large number
+isAntisym≤ : m ≤ n → n ≤ m → m ≡ n
+isAntisym≤ {pos zero}       {pos zero}       (pos≤pos p)       (pos≤pos q)       = refl
+isAntisym≤ {pos (suc m)}    {pos (suc n)}    (pos≤pos p)       (pos≤pos q)       =
+  cong sucℤ (isAntisym≤ (pos≤pos p) (pos≤pos q))
+isAntisym≤ {negsuc zero}    {negsuc zero}    (negsuc≤negsuc p) (negsuc≤negsuc q) = refl
+isAntisym≤ {negsuc (suc m)} {negsuc (suc n)} (negsuc≤negsuc p) (negsuc≤negsuc q) =
+  cong predℤ (isAntisym≤ (negsuc≤negsuc p) (negsuc≤negsuc q))
+
+≤Monotone+ : m ≤ n → o ≤ s → m ℤ.+ o ≤ n ℤ.+ s
+≤Monotone+ {n = n} p = isTrans≤ (≤-+o p) ∘ ≤-o+ {o = n}
+
+<Monotone+ : m < n → o < s → m ℤ.+ o < n ℤ.+ s
+<Monotone+ {n = n} p = isTrans< (<-+o p) ∘ <-o+ {o = n}
+
+≤-o+-cancel : o ℤ.+ m ≤ o ℤ.+ n → m ≤ n
+≤-o+-cancel {o} {m} {n} = recompute≤ ∘ subst2 _≤_
+  (ℤ.+Assoc (ℤ.- o) o m ∙∙ cong (ℤ._+ m) (ℤ.-Cancel' o) ∙∙ ℤ.+IdL m)
+  (ℤ.+Assoc (ℤ.- o) o n ∙∙ cong (ℤ._+ n) (ℤ.-Cancel' o) ∙∙ ℤ.+IdL n)
+  ∘ ≤-o+ {o = ℤ.- o}
+
+<-o+-cancel : o ℤ.+ m < o ℤ.+ n → m < n
+<-o+-cancel {o} {m} {n} = recompute< ∘ subst2 _<_
+  (ℤ.+Assoc (ℤ.- o) o m ∙∙ cong (ℤ._+ m) (ℤ.-Cancel' o) ∙∙ ℤ.+IdL m)
+  (ℤ.+Assoc (ℤ.- o) o n ∙∙ cong (ℤ._+ n) (ℤ.-Cancel' o) ∙∙ ℤ.+IdL n)
+  ∘ <-o+ {o = ℤ.- o}
+
+≤-+o-cancel : m ℤ.+ o ≤ n ℤ.+ o → m ≤ n
+≤-+o-cancel {m} {o} {n} = ≤-o+-cancel {o = o} ∘ subst2 _≤_ (ℤ.+Comm m o) (ℤ.+Comm n o)
+
+<-+o-cancel : m ℤ.+ o < n ℤ.+ o → m < n
+<-+o-cancel {m} {o} {n} = <-o+-cancel {o = o} ∘ subst2 _<_ (ℤ.+Comm m o) (ℤ.+Comm n o)
+
+≤-+pos-trans : m ℤ.+ pos k ≤ n → m ≤ n
+≤-+pos-trans = isTrans≤ ≤SumLeftPos
+
+≤-pos+-trans : pos k ℤ.+ m ≤ n → m ≤ n
+≤-pos+-trans = isTrans≤ ≤SumRightPos
+
+≤-·o : m ≤ n → m ℤ.· pos k ≤ n ℤ.· pos k
+≤-·o = recompute≤ ∘ proof _ _ _ where
+  proof : ∀ m n k → m ≤ n → m ℤ.· pos k ≤ n ℤ.· pos k
+  proof m n zero    _ = subst2 _≤_ (sym (ℤ.·AnnihilR m)) (sym (ℤ.·AnnihilR n)) zero-≤pos
+  proof (pos zero)       (pos zero)       (suc k) (pos≤pos p)       = zero-≤pos
+  proof (pos zero)       (pos (suc n))    (suc k) (pos≤pos p)       = zero-≤pos
+  proof (pos (suc m))    (pos (suc n))    (suc k) (pos≤pos p)       =
+    ≤-o+ {o = pos (suc k)} (proof (pos m) (pos n) (suc k) (pos≤pos p))
+  proof (negsuc m)       (pos n)          (suc k)  negsuc≤pos       = negsuc≤pos
+  proof (negsuc zero)    (negsuc zero)    (suc k) (negsuc≤negsuc p) = isRefl≤
+  proof (negsuc (suc m)) (negsuc zero)    (suc k) (negsuc≤negsuc p) =
+    pos≤pos→negsuc≥negsuc
+      (subst (_≤ pos k ℤ.+ pos (suc m ℕ.· suc k)) (sym (ℤ.+IdR (pos k))) ≤SumLeftPos)
+  proof (negsuc (suc m)) (negsuc (suc n)) (suc k) (negsuc≤negsuc p) =
+    subst2 _≤_
+      (sym (predℤ· (negsuc m) (pos (suc k)))) (sym (predℤ· (negsuc n) (pos (suc k))))
+      (≤-o+ {o = negsuc k} (proof (negsuc m) (negsuc n) (suc k) (negsuc≤negsuc p)))
+
+0≤o→≤-·o : 0 ≤ o → m ≤ n → m ℤ.· o ≤ n ℤ.· o
+0≤o→≤-·o (pos≤pos p) = ≤-·o
+
+<-·o : m < n → m ℤ.· pos (suc k) < n ℤ.· pos (suc k)
+<-·o = recompute< ∘ proof _ _ _ where
+  proof : ∀ m n k → m < n → m ℤ.· pos (suc k) < n ℤ.· pos (suc k)
+  proof (pos zero)       (pos (suc n))    k (pos<pos p)       = zero-<possuc
+  proof (pos (suc m))    (pos (suc n))    k (pos<pos p)       =
+    <-o+ {o = pos (suc k)} (proof (pos m) (pos n) k (pos<pos p))
+  proof (negsuc m)       (pos n)          k  negsuc<pos       = negsuc<pos
+  proof (negsuc (suc m)) (negsuc zero)    k (negsuc<negsuc p) =
+    pos<pos→negsuc>negsuc
+      (subst (_< pos k ℤ.+ pos (suc m ℕ.· suc k)) (sym (ℤ.+IdR (pos k))) <SumLeftPosSuc)
+  proof (negsuc (suc m)) (negsuc (suc n)) k (negsuc<negsuc p) =
+    subst2 _<_
+      (sym (predℤ· (negsuc m) (pos (suc k)))) (sym (predℤ· (negsuc n) (pos (suc k))))
+      (<-o+ {o = negsuc k} (proof (negsuc m) (negsuc n) k (negsuc<negsuc p)))
+
+0<o→<-·o : 0 < o → m < n → m ℤ.· o < n ℤ.· o
+0<o→<-·o {pos (suc k)} (pos<pos p) = <-·o
+
+<-weaken : m < n → m ≤ n
+<-weaken = <suc→≤ ∘ flip isTrans< <-sucℤ
+
+isIrrefl< : ¬ m < m
+isIrrefl< = recompute¬< $ proof _ where
+  proof : ∀ m → ¬ m < m
+  proof (pos (suc m))    (pos<pos p)       = proof (pos m)    (pos<pos p)
+  proof (negsuc (suc m)) (negsuc<negsuc p) = proof (negsuc m) (negsuc<negsuc p)
+
+pos≤0→≡0 : pos k ≤ 0 → pos k ≡ 0
+pos≤0→≡0 {zero} (pos≤pos x) = refl
+
+¬m+posk<m : ¬ m ℤ.+ pos k < m
+¬m+posk<m {m} {k} = recompute¬< $ ¬-pos<-zero ∘ <-o+-cancel {m} ∘ subst (m ℤ.+ pos k <_) (sym (ℤ.+IdR m))
+
+≤<-trans : o ≤ m → m < n → o < n
+≤<-trans p = suc≤→< ∘ isTrans≤ (suc-≤-suc p) ∘ <→suc≤
+
+<≤-trans : o < m → m ≤ n → o < n
+<≤-trans = (suc≤→< ∘_) ∘ isTrans≤ ∘ <→suc≤
+
+isAsym< : m < n → ¬ n ≤ m
+isAsym< = recompute¬≤ ∘ proof _ _ where
+  proof : ∀ m n → m < n → ¬ n ≤ m
+  proof (pos (suc m))    (pos (suc n))    (pos<pos p)       (pos≤pos q) =
+    proof (pos m) (pos n) (pos<pos p) (pos≤pos q)
+  proof (negsuc (suc m)) (negsuc (suc n)) (negsuc<negsuc p) (negsuc≤negsuc q) =
+    proof (negsuc m) (negsuc n) (negsuc<negsuc p) (negsuc≤negsuc q)
+
+isAsym'< : ¬ m < n → n ≤ m
+isAsym'< = recompute≤ ∘ proof _ _ where
+  proof : ∀ m n → ¬ m < n → n ≤ m
+  proof (pos m)          (pos zero)       ¬p = zero-≤pos
+  proof (pos zero)       (pos (suc n))    ¬p = ⊥.rec (¬p zero-<possuc)
+  proof (pos (suc m))    (pos (suc n))    ¬p =
+    suc-≤-suc (proof (pos m) (pos n) (¬p ∘ suc-<-suc))
+  proof (pos m)          (negsuc n)       ¬p = negsuc≤pos
+  proof (negsuc m)       (pos n)          ¬p = ⊥.rec (¬p negsuc<pos)
+  proof (negsuc zero)    (negsuc n)       ¬p = negsuc≤negsuc tt
+  proof (negsuc (suc m)) (negsuc zero)    ¬p = ⊥.rec (¬p (negsuc<negsuc tt))
+  proof (negsuc (suc m)) (negsuc (suc n)) ¬p =
+    pred-≤-pred (proof (negsuc m) (negsuc n) (¬p ∘ pred-<-pred))
+
+<-+pos-trans : m ℤ.+ pos k < n → m < n
+<-+pos-trans = ≤<-trans ≤SumLeftPos
+
+<-pos+-trans : pos k ℤ.+ m < n → m < n
+<-pos+-trans = ≤<-trans ≤SumRightPos
+
+<-+-≤ : m < n → o ≤ s → m ℤ.+ o < n ℤ.+ s
+<-+-≤ {n = n} p = <≤-trans (<-+o p) ∘ ≤-o+ {o = n}
+
+-Dist≤ : m ≤ n → (- n) ≤ (- m)
+-Dist≤ {pos zero}    {pos zero}    (pos≤pos p)       = pos≤pos tt
+-Dist≤ {pos zero}    {pos (suc n)} (pos≤pos p)       = negsuc≤pos
+-Dist≤ {pos (suc m)} {pos (suc n)} (pos≤pos p)       = negsuc≤negsuc p
+-Dist≤ {negsuc m}    {pos zero}     negsuc≤pos       = pos≤pos tt
+-Dist≤ {negsuc m}    {pos (suc n)}  negsuc≤pos       = negsuc≤pos
+-Dist≤ {negsuc m}    {negsuc n}    (negsuc≤negsuc p) = pos≤pos p
+
+-Dist< : m < n → (- n) < (- m)
+-Dist< {pos zero}    {pos (suc n)} (pos<pos p)       = negsuc<pos
+-Dist< {pos (suc m)} {pos (suc n)} (pos<pos p)       = negsuc<negsuc p
+-Dist< {negsuc m}    {pos zero}     negsuc<pos       = pos<pos tt
+-Dist< {negsuc m}    {pos (suc n)}  negsuc<pos       = negsuc<pos
+-Dist< {negsuc m}    {negsuc n}    (negsuc<negsuc p) = pos<pos p
+
+-pos≤ : m - (pos k) ≤ m
+-pos≤ {m} {k} = recompute≤ $ subst (m - pos k ≤_) (ℤ.+IdR m) (≤-o+ {o = m} (-Dist≤ zero-≤pos))
+
+≤→0≤Δ : m ≤ n → 0 ≤ n ℤ.- m
+≤→0≤Δ {m} {n} = recompute≤ ∘ subst (_≤ n ℤ.- m) (ℤ.-Cancel m) ∘ ≤-+o
+
+<→0<Δ : m < n → 0 < n ℤ.- m
+<→0<Δ {m} {n} = recompute< ∘ subst (_< n ℤ.- m) (ℤ.-Cancel m) ∘ <-+o
+
+0≤Δ→≤ : 0 ≤ n ℤ.- m → m ≤ n
+0≤Δ→≤ {n} {m} = recompute≤ ∘ subst2 _≤_ (ℤ.+IdL m) (ℤ.minusPlus m n) ∘ ≤-+o
+
+0<Δ→< : 0 < n ℤ.- m → m < n
+0<Δ→< {n} {m} = recompute< ∘ subst2 _<_ (ℤ.+IdL m) (ℤ.minusPlus m n) ∘ <-+o
+
+0≤→abs≡id : 0 ≤ n → pos (abs n) ≡ n
+0≤→abs≡id {pos n} _ = refl
+
+0<→abs≡id : 0 < n → pos (abs n) ≡ n
+0<→abs≡id {pos n} _ = refl
+
+·suc≤0 : m ℤ.· (pos (suc k)) ≤ 0 → m ≤ 0
+·suc≤0 {pos zero} (pos≤pos p) = pos≤pos tt
+·suc≤0 {negsuc n}  _          = negsuc≤pos
+
+·suc<0 : m ℤ.· (pos (suc k)) < 0 → m < 0
+·suc<0 {pos n}    (pos<pos ())
+·suc<0 {negsuc n}  _          = negsuc<pos
+
+0≤·suc-cancel : 0 ≤ m ℤ.· pos (suc k) → 0 ≤ m
+0≤·suc-cancel {pos n} _ = zero-≤pos
+
+0<·suc-cancel : 0 < m ℤ.· pos (suc k) → 0 < m
+0<·suc-cancel {pos (suc n)} (pos<pos p) = zero-<possuc
+
+0≤suc·-cancel : 0 ≤ pos (suc k) ℤ.· m → 0 ≤ m
+0≤suc·-cancel {m = pos n} _ = zero-≤pos
+
+0<suc·-cancel : 0 < pos (suc k) ℤ.· m → 0 < m
+0<suc·-cancel {k} {pos zero}    p = subst (0 <_) (ℤ.·AnnihilR (pos (suc k))) p
+0<suc·-cancel {k} {pos (suc n)} _ = zero-<possuc
+
+≤-·o-cancel : m ℤ.· pos (suc k) ≤ n ℤ.· pos (suc k) → m ≤ n
+≤-·o-cancel {m} {n = n} = 0≤Δ→≤ ∘ 0≤·suc-cancel
+  ∘ subst (0 ≤_) (cong (n ℤ.· _ ℤ.+_) (ℤ.-DistL· m _) ∙ sym (ℤ.·DistL+ n (ℤ.- m) _))
+  ∘ ≤→0≤Δ
+
+<-·o-cancel : m ℤ.· pos (suc k) < n ℤ.· pos (suc k) → m < n
+<-·o-cancel {m} {n = n} = 0<Δ→< ∘ 0<·suc-cancel
+  ∘ subst (0 <_) (cong (n ℤ.· _ ℤ.+_) (ℤ.-DistL· m _) ∙ sym (ℤ.·DistL+ n (ℤ.- m) _))
+  ∘ <→0<Δ
+
+0<o→≤-·o-cancel : 0 < o → m ℤ.· o ≤ n ℤ.· o → m ≤ n
+0<o→≤-·o-cancel {pos (suc k)} (pos<pos p) = ≤-·o-cancel
+
+0<o→<-·o-cancel : 0 < o → m ℤ.· o < n ℤ.· o → m < n
+0<o→<-·o-cancel {pos (suc k)} (pos<pos p) = <-·o-cancel
+
+≤-o·-cancel : (pos (suc k)) ℤ.· m ≤ (pos (suc k)) ℤ.· n → m ≤ n
+≤-o·-cancel {m = m} {n} = ≤-·o-cancel ∘ subst2 _≤_ (ℤ.·Comm _ m) (ℤ.·Comm _ n)
+
+<-o·-cancel : (pos (suc k)) ℤ.· m < (pos (suc k)) ℤ.· n → m < n
+<-o·-cancel {m = m} {n} = <-·o-cancel ∘ subst2 _<_ (ℤ.·Comm _ m) (ℤ.·Comm _ n)
+
+0<o→≤-o·-cancel : 0 < o → o ℤ.· m ≤ o ℤ.· n → m ≤ n
+0<o→≤-o·-cancel {pos (suc k)} (pos<pos p) = ≤-o·-cancel
+
+0<o→<-o·-cancel : 0 < o → o ℤ.· m < o ℤ.· n → m < n
+0<o→<-o·-cancel {pos (suc k)} (pos<pos p) = <-o·-cancel
+
+≤max : m ≤ ℤ.max m n
+≤max {pos zero}       {pos n}          = zero-≤pos
+≤max {pos (suc m)}    {pos zero}       = isRefl≤
+≤max {pos (suc m)}    {pos (suc n)} with m ℕ.<ᵇ n UsingEq
+... | false , p = isRefl≤
+... | true  , p = <-weaken (pos<pos (subst Bool→Type (sym p) tt))
+≤max {pos m}          {negsuc n}       = isRefl≤
+≤max {negsuc m}       {pos n}          = negsuc≤pos
+≤max {negsuc zero}    {negsuc n}       = isRefl≤
+≤max {negsuc (suc m)} {negsuc zero}    = negsuc≤negsuc tt
+≤max {negsuc (suc m)} {negsuc (suc n)} with m ℕ.<ᵇ n UsingEq
+... | false , p = isAsym'< (¬>ℕ→¬negsuc<negsuc (subst Bool→Type p))
+... | true  , p = isRefl≤
+
+-- this proof will not normalize quickly when m and n are the same large number
+≤→max : m ≤ n → ℤ.max m n ≡ n
+≤→max {pos zero}       {pos n}           p                = refl
+≤→max {pos (suc m)}    {pos (suc n)}    (pos≤pos p) with m ℕ.<ᵇ n UsingEq
+... | false , q = isAntisym≤ (pos≤pos p) (isAsym'< (¬<ℕ→¬pos<pos (subst Bool→Type q)) )
+... | true  , q = refl
+≤→max {negsuc m}       {pos n}           _                = refl
+≤→max {negsuc zero}    {negsuc zero}    (negsuc≤negsuc p) = refl
+≤→max {negsuc (suc m)} {negsuc zero}    (negsuc≤negsuc p) = refl
+≤→max {negsuc (suc m)} {negsuc (suc n)} (negsuc≤negsuc p) with m ℕ.<ᵇ n UsingEq
+... | false , q = refl
+... | true  , q = isAntisym≤ (negsuc≤negsuc p)
+                             (<-weaken (negsuc<negsuc (subst Bool→Type (sym q) tt)))
+
+min≤ : ℤ.min m n ≤ m
+min≤ {pos zero}       {pos n}          = zero-≤pos
+min≤ {pos (suc m)}    {pos zero}       = zero-≤pos
+min≤ {pos (suc m)}    {pos (suc n)} with m ℕ.<ᵇ n UsingEq
+... | false , p = isAsym'< (¬<ℕ→¬pos<pos (subst Bool→Type p))
+... | true  , p = isRefl≤
+min≤ {pos m}          {negsuc n}       = negsuc≤pos
+min≤ {negsuc m}       {pos n}          = isRefl≤
+min≤ {negsuc zero}    {negsuc n}       = negsuc≤negsuc tt
+min≤ {negsuc (suc m)} {negsuc zero}    = isRefl≤
+min≤ {negsuc (suc m)} {negsuc (suc n)} with m ℕ.<ᵇ n UsingEq
+... | false , p = isRefl≤
+... | true  , p = <-weaken (negsuc<negsuc (subst Bool→Type (sym p) tt))
+
+-- this proof will not normalize quickly when m and n are the same large number
+≤→min : m ≤ n → ℤ.min m n ≡ m
+≤→min {pos zero}       {pos n}           _                = refl
+≤→min {pos (suc m)}    {pos (suc n)}    (pos≤pos p) with m ℕ.<ᵇ n UsingEq
+... | false , q = isAntisym≤ (isAsym'< (¬<ℕ→¬pos<pos (subst Bool→Type q))) (pos≤pos p)
+... | true  , q = refl
+≤→min {negsuc m}       {pos n}           _                = refl
+≤→min {negsuc zero}    {negsuc zero}    (negsuc≤negsuc p) = refl
+≤→min {negsuc (suc m)} {negsuc zero}    (negsuc≤negsuc p) = refl
+≤→min {negsuc (suc m)} {negsuc (suc n)} (negsuc≤negsuc p) with m ℕ.<ᵇ n UsingEq
+... | false , q = refl
+... | true  , q = isAntisym≤ (<-weaken (negsuc<negsuc (subst Bool→Type (sym q) tt)))
+                             (negsuc≤negsuc p)
+
+≤MonotoneMin : m ≤ n → o ≤ s → ℤ.min m o ≤ ℤ.min n s
+≤MonotoneMin {m} {n} {o} {s} p q = recompute≤ $
+  subst (_≤ ℤ.min n s) (
+      sym (minAssoc n s (ℤ.min m o))
+    ∙ cong (ℤ.min n) (
+        minAssoc s m o ∙ cong (flip ℤ.min o) (ℤ.minComm s m) ∙ sym (minAssoc m s o))
+    ∙ minAssoc n m (ℤ.min s o)
+    ∙ cong₂ ℤ.min (ℤ.minComm n m ∙ ≤→min p)
+      (ℤ.minComm s o ∙ ≤→min q))
+    min≤
+
+≤MonotoneMax : m ≤ n → o ≤ s → ℤ.max m o ≤ ℤ.max n s
+≤MonotoneMax {m} {n} {o} {s} p q = recompute≤ $
+  subst (ℤ.max m o ≤_) (
+      sym (maxAssoc m o (ℤ.max n s)) ∙
+      cong (ℤ.max m) (
+        maxAssoc o n s
+      ∙ cong (flip ℤ.max s) (ℤ.maxComm o n)
+      ∙ sym (maxAssoc n o s)) ∙ maxAssoc m n (ℤ.max o s)
+      ∙ cong₂ ℤ.max (≤→max p) (≤→max q))
+    ≤max
+
+0<+ : ∀ m n → 0 < m ℤ.+ n → (0 < m) ⊎ (0 < n)
+0<+ (pos zero)    (pos (suc n)) (pos<pos p) = inr zero-<possuc
+0<+ (pos (suc m)) (pos zero)    (pos<pos p) = inl zero-<possuc
+0<+ (pos (suc m)) (pos (suc n)) (pos<pos p) = inr zero-<possuc -- alternative : inl zero-<possuc
+0<+ (pos (suc m)) (negsuc n)     _          = inl zero-<possuc
+0<+ (negsuc m)    (pos (suc n))  _          = inr zero-<possuc
+
+Σℕ→≤ : Σ[ k ∈ ℕ ] m ℤ.+ pos k ≡ n → m ≤ n
+Σℕ→≤ = recompute≤ ∘ uncurry λ _ → flip (subst (_ ≤_)) ≤SumLeftPos
+
+Σℕ→< : Σ[ k ∈ ℕ ] m ℤ.+ pos (suc k) ≡ n → m < n
+Σℕ→< = recompute< ∘ uncurry λ _ → flip (subst (_ <_)) <SumLeftPosSuc
+
+-- the first component will normalize quickly, but not the path itself
+≤→Σℕ : m ≤ n → Σ[ k ∈ ℕ ] m ℤ.+ pos k ≡ n
+≤→Σℕ {m} {n} p .fst = abs (n - m)
+≤→Σℕ {m} {n} p .snd =
+  m ℤ.+ pos (abs (n - m)) ≡⟨ cong (m ℤ.+_) (0≤→abs≡id (≤→0≤Δ p)) ⟩
+  m ℤ.+ (n - m)           ≡⟨ ℤ.+Comm m (n - m) ⟩
+  (n - m) ℤ.+ m           ≡⟨ ℤ.minusPlus m n ⟩
+  n                       ∎
+
+-- the first component will normalize quickly, but not the path itself
+<→Σℕ : m < n → Σ[ k ∈ ℕ ] m ℤ.+ pos (suc k) ≡ n
+<→Σℕ {m} = map-snd (sym (+sucℤ m _) ∙∙ sucℤ+ m _ ∙∙_) ∘ ≤→Σℕ ∘ <→suc≤
+
+data Trichotomy m n : Type where
+  lt : m < n → Trichotomy m n
+  eq : m ≡ n → Trichotomy m n
+  gt : n < m → Trichotomy m n
+
+Trichotomy-suc : Trichotomy m n → Trichotomy (sucℤ m) (sucℤ n)
+Trichotomy-suc (lt m<n) = lt (suc-<-suc m<n)
+Trichotomy-suc (eq m≡n) = eq (cong sucℤ m≡n)
+Trichotomy-suc (gt n<m) = gt (suc-<-suc n<m)
+
+Trichotomy-pred : Trichotomy (sucℤ m) (sucℤ n) → Trichotomy m n
+Trichotomy-pred (lt m<n) = lt (pred-<-pred m<n)
+Trichotomy-pred (eq m≡n) = eq (sym (predSuc _) ∙ cong predℤ m≡n ∙ predSuc _)
+Trichotomy-pred (gt n<m) = gt (pred-<-pred n<m)
+
+-- this proof will decide quickly among the cases `lt`, `gt`, `eq`
+-- however, the path for the proof of the `eq` case will normalize slowly
+_≟_ : ∀ m n → Trichotomy m n
+pos m    ≟ pos n with m ℕ.≟ n
+... | ℕ.lt p = lt $ recompute< $ pos<pos {m} {n} (ℕ.<→<ᵗ p)
+... | ℕ.eq p = eq (cong pos p)
+... | ℕ.gt p = gt $ recompute< $ pos<pos {n} {m} (ℕ.<→<ᵗ p)
+pos m    ≟ negsuc n = gt negsuc<pos
+negsuc m ≟ pos n    = lt negsuc<pos
+negsuc m ≟ negsuc n with m ℕ.≟ n
+... | ℕ.lt p = gt $ recompute< $ negsuc<negsuc {n} {m} (ℕ.<→<ᵗ p)
+... | ℕ.eq p = eq (cong negsuc p)
+... | ℕ.gt p = lt $ recompute< $ negsuc<negsuc {m} {n} (ℕ.<→<ᵗ p)
+
+-- alternative proof
+_≟'_ : ∀ m n → Trichotomy m n
+pos zero       ≟' pos zero       = eq refl
+pos zero       ≟' pos (suc n)    = lt zero-<possuc
+pos (suc m)    ≟' pos zero       = gt zero-<possuc
+pos (suc m)    ≟' pos (suc n)    = Trichotomy-suc (pos m ≟' pos n)
+pos m          ≟' negsuc n       = gt negsuc<pos
+negsuc m       ≟' pos n          = lt negsuc<pos
+negsuc zero    ≟' negsuc zero    = eq refl
+negsuc zero    ≟' negsuc (suc n) = gt (negsuc<negsuc tt)
+negsuc (suc m) ≟' negsuc zero    = lt (negsuc<negsuc tt)
+negsuc (suc m) ≟' negsuc (suc n) = Trichotomy-pred (negsuc m ≟' negsuc n)
+
+-- raw comparisons, without the proof terms
+compare : ℤ → ℤ → Ordering
+compare m n with m ≟ n
+... | lt _ = LT
+... | eq _ = EQ
+... | gt _ = GT
+
+compare' : ℤ → ℤ → Ordering
+compare' m n with m ≟' n
+... | lt _ = LT
+... | eq _ = EQ
+... | gt _ = GT
+
+private
+
+  test₀ : compare -4294967296  4295967296 ≡ LT
+  test₀ = refl
+
+  test₁ : compare -4294967296 -4294967296 ≡ EQ
+  test₁ = refl
+
+  test₂ : compare -4294967296 -4295967296 ≡ GT
+  test₂ = refl
+
+  test₀' : compare' -4294967296  4295967296 ≡ LT
+  test₀' = refl
+
+  {- This would take much longer to typecheck:
+
+  test₁' : compare' -4294967296 -4294967296 ≡ EQ
+  test₁' = refl
+
+  test₂' : compare' -4294967296 -4295967296 ≡ GT
+  test₂' = refl
+
+  -}
diff --git a/Cubical/Data/Fast/Int/Properties.agda b/Cubical/Data/Fast/Int/Properties.agda
new file mode 100644
index 0000000000..df7a6abb3b
--- /dev/null
+++ b/Cubical/Data/Fast/Int/Properties.agda
@@ -0,0 +1,1165 @@
+module Cubical.Data.Fast.Int.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Relation.Nullary
+
+open import Cubical.Relation.Binary.Order.Pseudolattice.Properties
+open import Cubical.Relation.Binary.Order.Pseudolattice.Instances.Nat
+
+open import Cubical.Data.Bool
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.NatPlusOne.Base as ℕ₊₁
+open import Cubical.Data.Nat as ℕ hiding (
+    +-assoc ; +-comm ; min ; max ; minComm ; maxComm)
+  renaming (_·_ to _·ℕ_; _+_ to _+ℕ_)
+open import Cubical.Data.Nat.Order as ℕ using ()
+open import Cubical.Data.Sum
+open import Cubical.Data.Fin.Base
+open import Cubical.Data.Fin.Properties
+
+open import Cubical.Data.Int.Base as ℤ
+  hiding (_+_ ; _·_ ; _-_ ; _ℕ-_ ; sumFinℤ ; sumFinℤId)
+open import Cubical.Data.Int.Properties as P public using (
+    sucPred ; predSuc ; injPos ; injNegsuc ; posNotnegsuc ; negsucNotpos ; injNeg
+  ; discreteℤ ; isSetℤ ; -pos ; -neg ; sucℤnegsucneg ; -sucℤ ; -predℤ
+  ; -Involutive ; isEquiv- ; predℤ+negsuc ; sucℤ+negsuc ; predℤ-pos
+  ; ind-assoc ; ind-comm ; sucPathℤ ; addEq ; predPathℤ ; subEq ; _+'_ ; isEquivAddℤ'
+  ; abs→⊎ ; ⊎→abs ; abs≡0 ; ¬x≡0→¬abs≡0 ; abs- ; 0≢1-ℤ ; clamp)
+
+open import Cubical.Data.Fast.Int.Base
+
+open MeetProperties ℕ≤Pseudolattice
+open JoinProperties ℕ≤Pseudolattice
+
+private
+  ℕ-lem : ∀ n m → (pos n +negsuc m) ≡ (n ℕ- suc m)
+  ℕ-lem zero          zero    = refl
+  ℕ-lem (suc zero)    zero    = refl
+  ℕ-lem (suc (suc n)) zero    = refl
+  ℕ-lem zero          (suc m) = cong predℤ (P.+Comm 0 (negsuc m))
+  ℕ-lem (suc n)       (suc m) = predℤ+negsuc m (pos (suc n)) ∙ ℕ-lem n m
+
++≡+f : ∀ n m → n ℤ.+ m ≡ n + m
++≡+f (pos n)    (pos m)    = sym (P.pos+ n m)
++≡+f (pos n)    (negsuc m) = ℕ-lem n m
++≡+f (negsuc n) (pos m)    = P.+Comm (negsuc n) (pos m) ∙ ℕ-lem m n
++≡+f (negsuc n) (negsuc m) = sym (P.neg+ (suc n) (suc m))
+                            ∙ cong negsuc (ℕ.+-suc _ _)
+
+·≡·f : ∀ n m → n ℤ.· m ≡ n · m
+·≡·f (pos n)       (pos m)       = sym (P.pos·pos n m)
+·≡·f (pos zero)    (negsuc m)    = refl
+·≡·f (pos (suc n)) (negsuc m)    = P.pos·negsuc (suc n) m
+                                  ∙ cong -_ (sym (P.pos·pos (suc n) (suc m)))
+·≡·f (negsuc n)    (pos zero)    = P.·AnnihilR (negsuc n)
+·≡·f (negsuc n)    (pos (suc m)) = P.negsuc·pos n (suc m)
+                                  ∙ cong -_ (sym (P.pos·pos (suc n) (suc m)))
+·≡·f (negsuc n)    (negsuc m)    = P.negsuc·negsuc n m
+                                  ∙ sym (P.pos·pos (suc n) (suc m))
+
+subst-f : (A : (ℤ → ℤ → ℤ) → (ℤ → ℤ → ℤ) → Type) → A ℤ._+_ ℤ._·_ → A _+_ _·_
+subst-f A = subst2 A (λ i x y → +≡+f x y i) (λ i x y → ·≡·f x y i)
+
+-- `subst-f` can be used to transport proofs from the standard to the fast operations:
+private
+  ·Assoc' : (x y z : ℤ) → x · (y · z) ≡ x · y · z
+  ·Assoc' x y z = subst-f (λ _+_ _·_ → (x · (y · z)) ≡ ((x · y) · z)) (P.·Assoc x y z)
+
+sucℤ[negsuc]-pos : ∀ k → sucℤ (negsuc k) ≡ - pos k
+sucℤ[negsuc]-pos zero    = refl
+sucℤ[negsuc]-pos (suc k) = refl
+
++IdL : ∀ z → 0 + z ≡ z
++IdL (pos n)    = refl
++IdL (negsuc n) = refl
+
++IdR : ∀ z → z + 0 ≡ z
++IdR (pos n)    = cong pos (+-zero n)
++IdR (negsuc n) = refl
+
+min : ℤ → ℤ → ℤ
+min (pos m)    (pos n)    = pos (ℕ.min m n)
+min (pos m)    (negsuc n) = negsuc n
+min (negsuc m) (pos n)    = negsuc m
+min (negsuc m) (negsuc n) = negsuc (ℕ.max m n)
+
+minComm : ∀ n m → min n m ≡ min m n
+minComm (pos m)    (pos n)    = cong pos (ℕ.minComm m n)
+minComm (pos m)    (negsuc n) = refl
+minComm (negsuc m) (pos n)    = refl
+minComm (negsuc m) (negsuc n) = cong negsuc (ℕ.maxComm m n)
+
+minIdem : ∀ n → min n n ≡ n
+minIdem (pos n)    = cong pos ∧Idem
+minIdem (negsuc n) = cong negsuc ∨Idem
+
+max : ℤ → ℤ → ℤ
+max (pos m)    (pos n)    = pos (ℕ.max m n )
+max (pos m)    (negsuc n) = pos m
+max (negsuc m) (pos n)    = pos n
+max (negsuc m) (negsuc n) = negsuc (ℕ.min m n)
+
+maxComm : ∀ m n → max m n ≡ max n m
+maxComm (pos m)    (pos n)    = cong pos (ℕ.maxComm m n)
+maxComm (pos m)    (negsuc n) = refl
+maxComm (negsuc m) (pos n)    = refl
+maxComm (negsuc m) (negsuc n) = cong negsuc (ℕ.minComm m n)
+
+maxIdem : ∀ n → max n n ≡ n
+maxIdem (pos n)    = cong pos ∨Idem
+maxIdem (negsuc n) = cong negsuc ∧Idem
+
+sucDistMin : ∀ m n → sucℤ (min m n) ≡ min (sucℤ m) (sucℤ n)
+sucDistMin (pos m)          (pos n)          = cong pos (sym minSuc)
+sucDistMin (pos m)          (negsuc zero)    = refl
+sucDistMin (pos m)          (negsuc (suc n)) = refl
+sucDistMin (negsuc zero)    (pos n)          = refl
+sucDistMin (negsuc (suc m)) (pos n)          = refl
+sucDistMin (negsuc zero)    (negsuc zero)    = refl
+sucDistMin (negsuc zero)    (negsuc (suc n)) = refl
+sucDistMin (negsuc (suc m)) (negsuc zero)    = refl
+sucDistMin (negsuc (suc m)) (negsuc (suc n)) = cong (sucℤ ∘ negsuc) maxSuc
+
+predDistMin : ∀ m n → predℤ (min m n) ≡ min (predℤ m) (predℤ n)
+predDistMin (pos zero)    (pos zero)    = refl
+predDistMin (pos zero)    (pos (suc n)) = refl
+predDistMin (pos (suc m)) (pos zero)    = refl
+predDistMin (pos (suc m)) (pos (suc n)) = cong (predℤ ∘ pos) minSuc
+predDistMin (pos zero)    (negsuc n)    = refl
+predDistMin (pos (suc m)) (negsuc n)    = refl
+predDistMin (negsuc m) (pos zero)       = refl
+predDistMin (negsuc m) (pos (suc n))    = refl
+predDistMin (negsuc m)    (negsuc n)    = cong negsuc (sym maxSuc)
+
+minSucL : ∀ m → min (sucℤ m) m ≡ m
+minSucL (pos m)          = cong pos (≥→∧≡Right ℕ.≤-sucℕ)
+minSucL (negsuc zero)    = refl
+minSucL (negsuc (suc m)) = cong negsuc (≤→∨≡Right ℕ.≤-sucℕ)
+
+minSucR : ∀ m → min m (sucℤ m)  ≡ m
+minSucR m = minComm m (sucℤ m) ∙ minSucL m
+
+minPredL : ∀ m → min (predℤ m) m ≡ predℤ m
+minPredL (pos zero)    = refl
+minPredL (pos (suc m)) = cong pos (≤→∧≡Left ℕ.≤-sucℕ)
+minPredL (negsuc m)    = cong negsuc (≥→∨≡Left ℕ.≤-sucℕ)
+
+minPredR : ∀ m → min m (predℤ m) ≡ predℤ m
+minPredR m = minComm m (predℤ m) ∙ minPredL m
+
+sucDistMax : ∀ m n → sucℤ (max m n) ≡ max (sucℤ m) (sucℤ n)
+sucDistMax (pos m)          (pos n)          = cong pos (sym maxSuc)
+sucDistMax (pos m)          (negsuc zero)    = refl
+sucDistMax (pos m)          (negsuc (suc n)) = refl
+sucDistMax (negsuc zero)    (pos n)          = refl
+sucDistMax (negsuc (suc m)) (pos n)          = refl
+sucDistMax (negsuc zero)    (negsuc zero)    = refl
+sucDistMax (negsuc zero)    (negsuc (suc n)) = refl
+sucDistMax (negsuc (suc m)) (negsuc zero)    = refl
+sucDistMax (negsuc (suc m)) (negsuc (suc n)) = cong (sucℤ ∘ negsuc) minSuc
+
+predDistMax : ∀ m n → predℤ (max m n) ≡ max (predℤ m) (predℤ n)
+predDistMax (pos zero)    (pos zero)    = refl
+predDistMax (pos zero)    (pos (suc n)) = refl
+predDistMax (pos (suc m)) (pos zero)    = refl
+predDistMax (pos (suc m)) (pos (suc n)) = cong (predℤ ∘ pos) maxSuc
+predDistMax (pos zero)    (negsuc n)    = refl
+predDistMax (pos (suc m)) (negsuc n)    = refl
+predDistMax (negsuc m)    (pos zero)    = refl
+predDistMax (negsuc m)    (pos (suc n)) = refl
+predDistMax (negsuc m)    (negsuc n)    = cong negsuc (sym minSuc)
+
+maxSucL : ∀ m → max (sucℤ m) m ≡ sucℤ m
+maxSucL (pos m)          = cong pos (≥→∨≡Left ℕ.≤-sucℕ)
+maxSucL (negsuc zero)    = refl
+maxSucL (negsuc (suc m)) = cong negsuc (≤→∧≡Left ℕ.≤-sucℕ)
+
+maxSucR : ∀ m → max m (sucℤ m) ≡ sucℤ m
+maxSucR m = maxComm m (sucℤ m) ∙ maxSucL m
+
+maxPredL : ∀ m → max (predℤ m) m ≡ m
+maxPredL (pos zero)    = refl
+maxPredL (pos (suc m)) = cong pos (≤→∨≡Right ℕ.≤-sucℕ)
+maxPredL (negsuc m)    = cong negsuc (≥→∧≡Right ℕ.≤-sucℕ)
+
+maxPredR : ∀ m → max m (predℤ m) ≡ m
+maxPredR m = maxComm m (predℤ m) ∙ maxPredL m
+
+minAssoc : ∀ x y z → min x (min y z) ≡ min (min x y) z
+minAssoc (pos m)    (pos n)    (pos k)    = cong pos $ ∧Assoc {m} {n} {k}
+minAssoc (pos m)    (pos n)    (negsuc k) = refl
+minAssoc (pos m)    (negsuc n) (pos k)    = refl
+minAssoc (pos m)    (negsuc n) (negsuc k) = refl
+minAssoc (negsuc m) (pos n)    (pos k)    = refl
+minAssoc (negsuc m) (pos n)    (negsuc k) = refl
+minAssoc (negsuc m) (negsuc n) (pos k)    = refl
+minAssoc (negsuc m) (negsuc n) (negsuc k) = cong negsuc $ ∨Assoc {m} {n} {k}
+
+maxAssoc : ∀ x y z → max x (max y z) ≡ max (max x y) z
+maxAssoc (pos m)    (pos n)    (pos k)    = cong pos $ ∨Assoc {m} {n} {k}
+maxAssoc (pos m)    (pos n)    (negsuc k) = refl
+maxAssoc (pos m)    (negsuc n) (pos k)    = refl
+maxAssoc (pos m)    (negsuc n) (negsuc k) = refl
+maxAssoc (negsuc m) (pos n)    (pos k)    = refl
+maxAssoc (negsuc m) (pos n)    (negsuc k) = refl
+maxAssoc (negsuc m) (negsuc n) (pos k)    = refl
+maxAssoc (negsuc m) (negsuc n) (negsuc k) = cong negsuc $ ∧Assoc {m} {n} {k}
+
+minAbsorbLMax : ∀ x y → min x (max x y) ≡ x
+minAbsorbLMax (pos zero) (pos n) = refl
+minAbsorbLMax (pos (suc m)) (pos zero) = cong pos ∧Idem
+minAbsorbLMax (pos (suc m)) (pos (suc n)) with m <ᵇ n UsingEq
+... | false , _ = cong pos ∧Idem
+... | true  , p  with m <ᵇ n UsingEq
+... | false , ¬p = ⊥.rec (true≢false (sym p ∙ ¬p))
+... | true  , _  = refl
+minAbsorbLMax (pos m)    (negsuc n) = cong pos ∧Idem
+minAbsorbLMax (negsuc m) (pos n)    = refl
+minAbsorbLMax (negsuc zero) (negsuc n) = refl
+minAbsorbLMax (negsuc (suc m)) (negsuc zero) = refl
+minAbsorbLMax (negsuc (suc m)) (negsuc (suc n)) with m <ᵇ n UsingEq
+... | true  , _ = cong negsuc ∨Idem
+... | false , ¬p with m <ᵇ n UsingEq
+... | false , _ = refl
+... | true  , p = ⊥.rec (true≢false (sym p ∙ ¬p))
+
+maxAbsorbLMin : ∀ x y → max x (min x y) ≡ x
+maxAbsorbLMin (pos zero) (pos n) = refl
+maxAbsorbLMin (pos (suc m)) (pos zero) = refl
+maxAbsorbLMin (pos (suc m)) (pos (suc n)) with m <ᵇ n UsingEq
+... | true  , _ = cong pos ∨Idem
+... | false , ¬p with m <ᵇ n UsingEq
+... | false , _ = refl
+... | true  , p = ⊥.rec (true≢false (sym p ∙ ¬p))
+maxAbsorbLMin (pos m) (negsuc n) = refl
+maxAbsorbLMin (negsuc m) (pos n) = cong negsuc ∧Idem
+maxAbsorbLMin (negsuc zero) (negsuc n) = refl
+maxAbsorbLMin (negsuc (suc m)) (negsuc zero) = cong negsuc ∧Idem
+maxAbsorbLMin (negsuc (suc m)) (negsuc (suc n)) with m <ᵇ n UsingEq
+... | false , _ = cong negsuc ∧Idem
+... | true  , p  with m <ᵇ n UsingEq
+... | false , ¬p = ⊥.rec (true≢false (sym p ∙ ¬p))
+... | true  , _  = refl
+
+predℤ+pos : ∀ n m → predℤ (m +pos n) ≡ (predℤ m) +pos n
+predℤ+pos zero m = refl
+predℤ+pos (suc n) m =
+  predℤ (sucℤ (m +pos n))   ≡⟨ predSuc _ ⟩
+  m +pos n                  ≡[ i ]⟨ sucPred m (~ i) +pos n ⟩
+  (sucℤ (predℤ m)) +pos n   ≡⟨ sym (P.sucℤ+pos n (predℤ m))⟩
+  (predℤ m) +pos (suc n)    ∎
+
+predℕ-≡ℕ-suc : ∀ m n → predℤ (m ℕ- n) ≡ m ℕ- (suc n)
+predℕ-≡ℕ-suc zero          zero    = refl
+predℕ-≡ℕ-suc zero          (suc n) = refl
+predℕ-≡ℕ-suc (suc zero)    zero    = refl
+predℕ-≡ℕ-suc (suc (suc m)) zero    = refl
+predℕ-≡ℕ-suc (suc m)       (suc n) = predℕ-≡ℕ-suc m n
+
+predℤ+ : ∀ m n → predℤ (m + n) ≡ (predℤ m) + n
+predℤ+ (pos zero)    (pos zero)          = refl
+predℤ+ (pos zero)    (pos (suc zero))    = refl
+predℤ+ (pos zero)    (pos (suc (suc n))) = refl
+predℤ+ (pos (suc m)) (pos n)             = refl
+predℤ+ (pos zero)    (negsuc n)          = refl
+predℤ+ (pos (suc m)) (negsuc n)          = predℕ-≡ℕ-suc m n
+predℤ+ (negsuc m)    (pos n)             = predℕ-≡ℕ-suc n (suc m)
+predℤ+ (negsuc m)    (negsuc n)          = refl
+
++predℤ : ∀ m n → predℤ (m + n) ≡ m + (predℤ n)
++predℤ (pos zero)          (pos zero)    = refl
++predℤ (pos (suc zero))    (pos zero)    = refl
++predℤ (pos (suc (suc m))) (pos zero)    = cong (pos ∘ suc) (ℕ.+-zero m)
++predℤ (pos m)             (pos (suc n)) = cong (predℤ ∘ pos) (ℕ.+-comm m (suc n)) ∙ cong pos (ℕ.+-comm n m)
++predℤ (pos m)             (negsuc n)    = predℕ-≡ℕ-suc m (suc n)
++predℤ (negsuc m)          (pos zero)    = cong (negsuc ∘ suc) (sym (ℕ.+-zero m))
++predℤ (negsuc m)          (pos (suc n)) = predℕ-≡ℕ-suc n m
++predℤ (negsuc m)          (negsuc n)    = cong (negsuc ∘ suc ∘ suc ) (ℕ.+-comm m n)
+                                         ∙ cong (negsuc ∘ suc) (ℕ.+-comm (suc n) m)
+
+sucℕ-suc≡ℕ- : ∀ m n → sucℤ (m ℕ- suc n) ≡ m ℕ- n
+sucℕ-suc≡ℕ- zero          zero    = refl
+sucℕ-suc≡ℕ- zero          (suc n) = refl
+sucℕ-suc≡ℕ- (suc zero)    zero    = refl
+sucℕ-suc≡ℕ- (suc (suc m)) zero    = refl
+sucℕ-suc≡ℕ- (suc m)       (suc n) = sucℕ-suc≡ℕ- m n
+
+sucℤ+pos : ∀ n m → sucℤ (m + pos n) ≡ (sucℤ m) + pos n
+sucℤ+pos n (pos m)                   = refl
+sucℤ+pos zero (negsuc m)             = sym (+IdR (sucℤ (negsuc m + pos zero)))
+sucℤ+pos (suc zero) (negsuc zero)    = refl
+sucℤ+pos (suc (suc n)) (negsuc zero) = cong (sucℤ ∘ (ℕ-hlp (suc n))) (zero∸ (suc n))
+sucℤ+pos (suc n) (negsuc (suc m))    = w n m where
+  w : ∀ n m → sucℤ (ℕ-hlp (n ∸ suc m) (suc m ∸ n)) ≡ ℕ-hlp (n ∸ m) (m ∸ n)
+  w zero zero          = refl
+  w zero (suc m)       = refl
+  w (suc zero) zero    = refl
+  w (suc (suc n)) zero = cong (sucℤ ∘ (ℕ-hlp (suc n))) (zero∸ (suc n))
+  w (suc n) (suc m)    = w n m
+
+sucℤ+ : ∀ m n → sucℤ (m + n) ≡ (sucℤ m) + n
+sucℤ+ (pos m)          (pos n)             = refl
+sucℤ+ (pos m)          (negsuc n)          = sucℕ-suc≡ℕ- m n
+sucℤ+ (negsuc zero)    (pos zero)          = refl
+sucℤ+ (negsuc zero)    (pos (suc zero))    = refl
+sucℤ+ (negsuc zero)    (pos (suc (suc n))) = refl
+sucℤ+ (negsuc (suc m)) (pos n)             = sucℕ-suc≡ℕ- n (suc m)
+sucℤ+ (negsuc zero)    (negsuc n)          = refl
+sucℤ+ (negsuc (suc m)) (negsuc n)          = refl
+
++sucℤ : ∀ m n → sucℤ (m + n) ≡ m + (sucℤ n)
++sucℤ (pos m)             (pos n)          = cong (pos ∘ suc) (ℕ.+-comm m n) ∙ cong pos (ℕ.+-comm (suc n) m)
++sucℤ (pos zero)          (negsuc zero)    = refl
++sucℤ (pos (suc zero))    (negsuc zero)    = refl
++sucℤ (pos (suc (suc m))) (negsuc zero)    = cong (pos ∘ suc) (sym (ℕ.+-zero (suc m)))
++sucℤ (pos m)             (negsuc (suc n)) = sucℕ-suc≡ℕ- m (suc n)
++sucℤ (negsuc m)          (pos n)          = sucℕ-suc≡ℕ- n m
++sucℤ (negsuc m)          (negsuc zero)    = cong negsuc (ℕ.+-zero m)
++sucℤ (negsuc m)          (negsuc (suc n)) = cong negsuc (ℕ.+-comm m (suc n) ∙ cong suc (ℕ.+-comm n m))
+
+pos0+ : ∀ z → z ≡ pos 0 + z
+pos0+ (pos n)    = refl
+pos0+ (negsuc n) = refl
+
++pos0 : ∀ z → z ≡ z + pos 0
++pos0 (pos n)    = cong pos $ sym (ℕ.+-zero n)
++pos0 (negsuc n) = refl
+
+
+negsuc0+ : ∀ z → predℤ z ≡ negsuc 0 + z
+negsuc0+ (pos zero)          = refl
+negsuc0+ (pos (suc zero))    = refl
+negsuc0+ (pos (suc (suc n))) = refl
+negsuc0+ (negsuc n)          = refl
+
++negsuc0 : ∀ z → predℤ z ≡ z + negsuc 0
++negsuc0 (pos zero)          = refl
++negsuc0 (pos (suc zero))    = refl
++negsuc0 (pos (suc (suc n))) = refl
++negsuc0 (negsuc n)          = cong (negsuc ∘ suc) $ sym (ℕ.+-zero n)
+
++Comm : ∀ m n → m + n ≡ n + m
++Comm (pos m)    (pos n)     = cong pos (ℕ.+-comm m n)
++Comm (negsuc m) (pos n)     = refl
++Comm (pos m)    (negsuc n)  = refl
++Comm (negsuc m) (negsuc n)  = cong (negsuc ∘ suc) (ℕ.+-comm m n)
+
++Comm' : ∀ m n → m + n ≡ n + m
++Comm' m (pos n)    = ind-comm _+_ pos    sucℤ  refl sucℤ+  +sucℤ (λ n → sym (+pos0 n) ∙ pos0+ n) m n
++Comm' m (negsuc n) = ind-comm _+_ negsuc predℤ refl predℤ+ +predℤ (λ n → sym (+negsuc0 n) ∙ negsuc0+ n) m n
+
++Assoc' : ∀ m n o → m + (n + o) ≡ (m + n) + o
++Assoc' m n (pos o)    = ind-assoc _+_ pos    sucℤ  +sucℤ  refl (λ m n → sym (+pos0 (m + n)) ∙ cong (m +_) (+pos0 n) ) m n o
++Assoc' m n (negsuc o) = ind-assoc _+_ negsuc predℤ +predℤ refl (λ m n → sym (+negsuc0 (m + n))
+                                                                      ∙∙ +predℤ m n
+                                                                      ∙∙ cong (m +_) (+negsuc0 n) ) m n o
+
+nℕ-n≡0 : ∀ n → n ℕ- n ≡ pos 0
+nℕ-n≡0 zero    = refl
+nℕ-n≡0 (suc n) = nℕ-n≡0 n
+
++PosDistLℕ- : ∀ m n k → (n ℕ- k) + (pos m) ≡ (n ℕ.+ m) ℕ- k
++PosDistLℕ- zero    zero    zero    = refl
++PosDistLℕ- (suc m) zero    zero    = refl
++PosDistLℕ- m       zero    (suc k) = refl
++PosDistLℕ- m       (suc n) zero    = refl
++PosDistLℕ- m       (suc n) (suc k) = +PosDistLℕ- m n k
+
++PosDistRℕ- : ∀ m n k → (pos m) + (n ℕ- k) ≡ (m ℕ.+ n) ℕ- k
++PosDistRℕ- m n k = +Comm (pos m) (n ℕ- k)
+                 ∙∙ +PosDistLℕ- m n k
+                 ∙∙ cong (_ℕ- k) (ℕ.+-comm n m)
+
++NegsucDistLℕ- : ∀ m n k → (n ℕ- k) + negsuc m ≡ n ℕ- (suc k ℕ.+ m)
++NegsucDistLℕ- m zero zero       = refl
++NegsucDistLℕ- m zero (suc k)    = refl
++NegsucDistLℕ- m (suc n) zero    = refl
++NegsucDistLℕ- m (suc n) (suc k) = +NegsucDistLℕ- m n k
+
++NegsucDistRℕ- : ∀ m n k → negsuc m + (n ℕ- k) ≡ n ℕ- (suc m ℕ.+ k)
++NegsucDistRℕ- m n k = +Comm (negsuc m) (n ℕ- k)
+                    ∙∙ +NegsucDistLℕ- m n k
+                    ∙∙ cong (n ℕ-_ ∘ suc) (ℕ.+-comm k m)
+
++Assoc : ∀ m n k → m + (n + k) ≡ (m + n) + k
++Assoc (pos m)    (pos n)    (pos k)    = cong pos (ℕ.+-assoc m n k)
++Assoc (pos m)    (pos n)    (negsuc k) = +PosDistRℕ- m n (suc k)
++Assoc (pos m)    (negsuc n) (pos k)    =
+  pos m + k ℕ- suc n ≡⟨ +PosDistRℕ- m k (suc n) ⟩
+  (m +ℕ k) ℕ- suc n  ≡⟨ sym (+PosDistLℕ- k m (suc n)) ⟩
+  m ℕ- suc n + pos k ∎
++Assoc (pos m)    (negsuc n) (negsuc k) = sym $ +NegsucDistLℕ- k m (suc n)
++Assoc (negsuc m) (pos n)    (pos k)    = sym $ +PosDistLℕ- k n (suc m)
++Assoc (negsuc m) (pos n)    (negsuc k) =
+  negsuc m + n ℕ- suc k   ≡⟨ +NegsucDistRℕ- m n (suc k) ⟩
+  n ℕ- (suc m +ℕ suc k)   ≡⟨ cong (n ℕ-_ ∘ suc) (ℕ.+-suc m k) ⟩
+  n ℕ- (suc (suc m) +ℕ k) ≡⟨ sym $ +NegsucDistLℕ- k n (suc m) ⟩
+  n ℕ- suc m + negsuc k   ∎
++Assoc (negsuc m) (negsuc n) (pos k)    = +NegsucDistRℕ- m k (suc n) ∙ cong (k ℕ-_ ∘ suc) (ℕ.+-suc m n)
++Assoc (negsuc m) (negsuc n) (negsuc k) = cong (negsuc ∘ suc) $
+  m +ℕ suc (n +ℕ k)   ≡⟨ ℕ.+-suc m (n +ℕ k) ⟩
+  suc (m +ℕ (n +ℕ k)) ≡⟨ cong suc (ℕ.+-assoc m n k)  ⟩
+  suc (m +ℕ n +ℕ k)   ∎
+
++'≡+ : _+'_ ≡ _+_
++'≡+ =  P.+'≡+ ∙ (λ i x y → +≡+f x y i)
+
+isEquivAddℤ : (m : ℤ) → isEquiv (λ n → n + m)
+isEquivAddℤ = subst (λ add → (m : ℤ) → isEquiv (λ n → add n m)) +'≡+ P.isEquivAddℤ'
+
+-- below is an alternate proof of isEquivAddℤ for comparison
+-- We also have two useful lemma here.
+
+-Cancel : ∀ z → z - z ≡ 0
+-Cancel (pos zero) = refl
+-Cancel (pos (suc n)) = nℕ-n≡0 n
+-Cancel (negsuc n) = nℕ-n≡0 n
+
+-Cancel' : ∀ z → - z + z ≡ 0
+-Cancel' z = +Comm (- z) z ∙ -Cancel z
+
+minusPlus : ∀ m n → (n - m) + m ≡ n
+minusPlus m n = (sym (+Assoc n (- m) m))
+             ∙∙ cong (n +_) (-Cancel' m)
+             ∙∙ sym (+pos0 n)
+
+plusMinus : ∀ m n → (n + m) - m ≡ n
+plusMinus m n = sym (+Assoc n m (- m))
+             ∙∙ cong (n +_) (-Cancel m)
+             ∙∙ sym (+pos0 n)
+
+private
+  alternateProof : (m : ℤ) → isEquiv (λ n → n + m)
+  alternateProof m = isoToIsEquiv (iso (λ n → n + m)
+                                       (λ n → n - m)
+                                       (minusPlus m)
+                                       (plusMinus m))
+
+-≡0 : (m n : ℤ) → m - n ≡ 0 → m ≡ n
+-≡0 m n p =
+  m         ≡⟨ sym (minusPlus n m) ⟩
+  m - n + n ≡⟨ cong (_+ n) p  ⟩
+  pos 0 + n ≡⟨ sym (pos0+ n) ⟩
+  n         ∎
+
+pos+ : ∀ m n → pos (m +ℕ n) ≡ pos m + pos n
+pos+ m n = refl
+
+negsuc+ : ∀ m n → negsuc (m +ℕ n) ≡ negsuc m - pos n
+negsuc+ m zero    = cong negsuc (ℕ.+-zero m)
+negsuc+ m (suc n) = cong negsuc (ℕ.+-suc m n)
+
+neg+ : ∀ m n → neg (m +ℕ n) ≡ neg m + neg n
+neg+ zero    zero    = refl
+neg+ zero    (suc n) = refl
+neg+ (suc m) zero    = cong negsuc (ℕ.+-zero m)
+neg+ (suc m) (suc n) = cong negsuc (ℕ.+-suc m n)
+
+ℕ-AntiComm : ∀ m n → m ℕ- n ≡ -(n ℕ- m)
+ℕ-AntiComm zero    zero    = refl
+ℕ-AntiComm zero    (suc n) = refl
+ℕ-AntiComm (suc m) zero    = refl
+ℕ-AntiComm (suc m) (suc n) = ℕ-AntiComm m n
+
+pos- : ∀ m n → m ℕ- n ≡ pos m - pos n
+pos- zero    zero    = refl
+pos- (suc m) zero    = cong (pos ∘ suc) (sym (ℕ.+-zero m))
+pos- m       (suc n) = refl
+
+-AntiComm : ∀ m n → m - n ≡ - (n - m)
+-AntiComm (pos m)       (pos n)       = sym (pos- m n) ∙∙ ℕ-AntiComm m n ∙∙ cong -_ (pos- n m)
+-AntiComm (pos zero)    (negsuc n)    = refl
+-AntiComm (pos (suc m)) (negsuc n)    = cong (pos ∘ suc) (ℕ.+-comm m (suc n))
+-AntiComm (negsuc m)    (pos zero)    = refl
+-AntiComm (negsuc m)    (pos (suc n)) = cong negsuc (ℕ.+-comm (suc m) n)
+-AntiComm (negsuc m)    (negsuc n)    = ℕ-AntiComm n m
+
+-Dist+ : ∀ m n → - (m + n) ≡ (- m) + (- n)
+-Dist+ (pos zero)    (pos zero)    = refl
+-Dist+ (pos zero)    (pos (suc n)) = refl
+-Dist+ (pos (suc m)) (pos zero)    = cong negsuc (ℕ.+-zero m)
+-Dist+ (pos (suc m)) (pos (suc n)) = cong negsuc (ℕ.+-suc m n)
+-Dist+ (pos zero)    (negsuc n)    = refl
+-Dist+ (pos (suc m)) (negsuc n)    = sym (ℕ-AntiComm n m)
+-Dist+ (negsuc m)    (pos zero)    = cong (pos ∘ suc) $ sym $ ℕ.+-zero m
+-Dist+ (negsuc m)    (pos (suc n)) = sym (ℕ-AntiComm m n)
+-Dist+ (negsuc m)    (negsuc n)    = cong (pos ∘ suc) $ sym $ ℕ.+-suc m n
+
+-DistMin : ∀ m n → - min m n ≡ max (- m) (- n)
+-DistMin (pos zero)    (pos zero)    = refl
+-DistMin (pos zero)    (pos (suc n)) = refl
+-DistMin (pos (suc m)) (pos zero)    = refl
+-DistMin (pos (suc m)) (pos (suc n)) = cong (-_ ∘ pos) minSuc
+-DistMin (pos zero)    (negsuc n)    = refl
+-DistMin (pos (suc m)) (negsuc n)    = refl
+-DistMin (negsuc m)    (pos zero)    = refl
+-DistMin (negsuc m)    (pos (suc n)) = refl
+-DistMin (negsuc m)    (negsuc n)    = cong pos (sym $ ℕ.maxSuc)
+
+-DistMax : ∀ m n → - max m n ≡ min (- m ) (- n)
+-DistMax m n = sym (cong₂ (λ x y → - (max x y)) (-Involutive m) (-Involutive n))
+            ∙∙ (sym $ cong -_ (-DistMin (- m) (- n)))
+            ∙∙ -Involutive (min (- m) (- n))
+
+min- : ∀ x y → min (pos x) (- (pos y)) ≡ - (pos y)
+min- zero    zero    = refl
+min- zero    (suc y) = refl
+min- (suc x) zero    = refl
+min- (suc x) (suc y) = refl
+
+-min : ∀ x y → min (- (pos x)) (pos y) ≡ - (pos x)
+-min x y = minComm (- (pos x)) (pos y) ∙ min- y x
+
+max- : ∀ x y → max (pos x) (- (pos y)) ≡ pos x
+max- zero    zero    = refl
+max- zero    (suc y) = refl
+max- (suc x) zero    = refl
+max- (suc x) (suc y) = refl
+
+-max : ∀ x y → max (- (pos x)) (pos y) ≡ pos y
+-max x y = maxComm (- (pos x)) (pos y) ∙ max- y x
+
+inj-z+ : ∀ {z l n} → z + l ≡ z + n → l ≡ n
+inj-z+ {z} {l} {n} p =
+  l             ≡⟨ pos0+ l ⟩
+  0 + l         ≡⟨ cong (_+ l) (sym (-Cancel' z)) ⟩
+  - z + z + l   ≡⟨ sym (+Assoc (- z) z l)  ⟩
+  - z + (z + l) ≡⟨ cong (- z +_) p ⟩
+  - z + (z + n) ≡⟨ +Assoc (- z) z n ⟩
+  - z + z + n   ≡⟨ cong (_+ n) (-Cancel' z) ⟩
+  0 + n         ≡⟨ sym (pos0+ n) ⟩
+  n             ∎
+
+inj-+z : ∀ {z l n} → l + z ≡ n + z → l ≡ n
+inj-+z {z} {l} {n} p = inj-z+ {z = z} {l} {n} (+Comm z l ∙∙ p ∙∙ +Comm n z)
+
+n+z≡z→n≡0 : ∀ n z → n + z ≡ z → n ≡ 0
+n+z≡z→n≡0 n z p = inj-z+ {z = z} {l = n} {n = 0} (+Comm z n ∙∙ p ∙∙ +pos0 z)
+
+pos+posLposMin : ∀ x y → min (pos (x +ℕ y)) (pos x) ≡ pos x
+pos+posLposMin zero y = minComm (pos y) (pos zero)
+pos+posLposMin (suc x) y = cong pos minSuc ∙ cong sucℤ (pos+posLposMin x y)
+
+pos+posRposMin : ∀ x y → min (pos x) (pos (x +ℕ y)) ≡ pos x
+pos+posRposMin x y = minComm (pos x) (pos (x +ℕ y)) ∙ pos+posLposMin x y
+
+pos+posLposMax : ∀ x y → max (pos (x +ℕ y)) (pos x) ≡ pos (x +ℕ y)
+pos+posLposMax zero y = maxComm (pos y) (pos zero)
+pos+posLposMax (suc x) y = cong pos maxSuc ∙ cong sucℤ (pos+posLposMax x y)
+
+pos+posRposMax : ∀ x y → max (pos x) (pos (x +ℕ y)) ≡ pos (x +ℕ y)
+pos+posRposMax x y = maxComm (pos x) (pos (x +ℕ y)) ∙ pos+posLposMax x y
+
+negsuc+posLnegsucMin : ∀ x y → min (negsuc x + pos y) (negsuc x) ≡ negsuc x
+negsuc+posLnegsucMin zero    zero          = refl
+negsuc+posLnegsucMin zero    (suc zero)    = refl
+negsuc+posLnegsucMin zero    (suc (suc y)) = refl
+negsuc+posLnegsucMin (suc x) zero          = minIdem (negsuc (suc x))
+negsuc+posLnegsucMin (suc x) (suc y)
+  = cong (flip min _)
+         (sym $ predℤ+ (negsuc x) (pos (suc y))) ∙∙
+    sym (predDistMin (negsuc x + pos (suc y)) (negsuc x)) ∙∙
+    cong predℤ (negsuc+posLnegsucMin x (suc y))
+
+negsuc+posRnegsucMin : ∀ x y → min (negsuc x) (negsuc x + pos y) ≡ negsuc x
+negsuc+posRnegsucMin x y = minComm (negsuc x) (negsuc x + pos y) ∙ negsuc+posLnegsucMin x y
+
+negsuc+posLnegsucMax : ∀ x y → max (negsuc x + pos y) (negsuc x) ≡ negsuc x + pos y
+negsuc+posLnegsucMax zero    zero          = refl
+negsuc+posLnegsucMax zero    (suc zero)    = refl
+negsuc+posLnegsucMax zero    (suc (suc y)) = refl
+negsuc+posLnegsucMax (suc x) zero          = maxIdem (negsuc (suc x))
+negsuc+posLnegsucMax (suc x) (suc y)
+  = cong (flip max _)
+         (sym $ predℤ+ (negsuc x) (pos (suc y))) ∙
+    sym (predDistMax (negsuc x + pos (suc y)) (negsuc x)) ∙
+    cong predℤ (negsuc+posLnegsucMax x (suc y)) ∙
+    predℤ+ (negsuc x) (pos (suc y))
+
+negsuc+posRnegsucMax : ∀ x y → max (negsuc x) (negsuc x + pos y) ≡ negsuc x + pos y
+negsuc+posRnegsucMax x y = maxComm (negsuc x) (negsuc x + pos y) ∙ negsuc+posLnegsucMax x y
+
+--  the following hold definitionally:
+
+negsuc+negsucLposMin : ∀ x y z → min (negsuc x + negsuc y) (pos z) ≡ negsuc x + negsuc y
+negsuc+negsucLposMin x y z = refl
+
+negsuc+negsucRposMin : ∀ x y z → min (pos x) (negsuc y + negsuc z) ≡ negsuc y + negsuc z
+negsuc+negsucRposMin z x y = refl
+
+negsuc+negsucLposMax : ∀ x y z → max (negsuc x + negsuc y) (pos z) ≡ pos z
+negsuc+negsucLposMax x y z = refl
+
+negsuc+negsucRposMax : ∀ x y z → max (pos x) (negsuc y + negsuc z) ≡ pos x
+negsuc+negsucRposMax z x y = refl
+
+
+negsuc+negsucLnegsucMin : ∀ x y → min (negsuc x + negsuc y) (negsuc x) ≡ negsuc x + negsuc y
+negsuc+negsucLnegsucMin zero    y = refl
+negsuc+negsucLnegsucMin (suc x) y = cong negsuc maxSuc ∙ cong predℤ (negsuc+negsucLnegsucMin x y)
+
+negsuc+negsucRnegsucMin : ∀ x y → min (negsuc x) (negsuc x + negsuc y) ≡ negsuc x + negsuc y
+negsuc+negsucRnegsucMin x y = minComm (negsuc x) (negsuc x + negsuc y) ∙ negsuc+negsucLnegsucMin x y
+
+negsuc+negsucLnegsucMax : ∀ x y → max (negsuc x + negsuc y) (negsuc x) ≡ negsuc x
+negsuc+negsucLnegsucMax zero zero    = refl
+negsuc+negsucLnegsucMax zero (suc y) = refl
+negsuc+negsucLnegsucMax (suc x) zero
+  = cong (flip max (negsuc (suc x)) ∘ negsuc ∘ suc ∘ suc) (+-zero x) ∙
+    maxPredL (negsuc (suc x))
+negsuc+negsucLnegsucMax (suc x) (suc y)
+  = cong (flip max _)
+         (sym $ predℤ+ (negsuc x) (negsuc (suc y))) ∙∙
+    sym (predDistMax (negsuc x + negsuc (suc y)) (negsuc x)) ∙∙
+    cong predℤ (negsuc+negsucLnegsucMax x (suc y))
+
+negsuc+negsucRnegsucMax : ∀ x y → max (negsuc x) (negsuc x + negsuc y) ≡ negsuc x
+negsuc+negsucRnegsucMax x y = maxComm (negsuc x) (negsuc x + negsuc y) ∙ negsuc+negsucLnegsucMax x y
+
+pos+pospos+negsucMin : ∀ x y z → min (pos x + pos y) (pos x + negsuc z) ≡ pos x + negsuc z
+pos+pospos+negsucMin zero x y = refl
+pos+pospos+negsucMin (suc x) y z
+  = cong₂ min (sym (sucℤ+ (pos x) (pos y)))
+              (sym (sucℤ+ (pos x) (negsuc z))) ∙
+    sym (sucDistMin (pos x + pos y) (pos x + negsuc z)) ∙
+    cong sucℤ (pos+pospos+negsucMin x y z) ∙
+    sucℤ+ (pos x) (negsuc z)
+
+pos+pospos+negsucMax : ∀ x y z → max (pos x + pos y) (pos x + negsuc z) ≡ pos x + pos y
+pos+pospos+negsucMax zero y z = refl
+pos+pospos+negsucMax (suc x) y z
+  = cong₂ max (sym (sucℤ+ (pos x) (pos y)))
+              (sym (sucℤ+ (pos x) (negsuc z))) ∙
+    sym (sucDistMax (pos x + pos y) (pos x + negsuc z)) ∙
+    cong sucℤ (pos+pospos+negsucMax x y z) ∙ sucℤ+ (pos x) (pos y)
+
+negsuc+negsucnegsuc+posMin : ∀ x y z → min (negsuc x + negsuc y) (negsuc x + pos z)
+                           ≡ negsuc x + negsuc y
+negsuc+negsucnegsuc+posMin zero zero    zero          = refl
+negsuc+negsucnegsuc+posMin zero zero    (suc zero)    = refl
+negsuc+negsucnegsuc+posMin zero zero    (suc (suc z)) = refl
+negsuc+negsucnegsuc+posMin zero (suc y) zero          = refl
+negsuc+negsucnegsuc+posMin zero (suc y) (suc zero)    = refl
+negsuc+negsucnegsuc+posMin zero (suc y) (suc (suc z)) = refl
+negsuc+negsucnegsuc+posMin (suc x) y z
+  = cong₂ min (sym (predℤ+ (negsuc x) (negsuc y)))
+              (sym (predℤ+ (negsuc x) (pos z))) ∙
+    sym (predDistMin (negsuc x + negsuc y) (negsuc x + pos z)) ∙
+    cong predℤ (negsuc+negsucnegsuc+posMin x y z) ∙
+    predℤ+ (negsuc x) (negsuc y)
+
+negsuc+negsucnegsuc+posMax : ∀ x y z → max (negsuc x + negsuc y) (negsuc x + pos z)
+                           ≡ negsuc x + pos z
+negsuc+negsucnegsuc+posMax zero zero    zero          = refl
+negsuc+negsucnegsuc+posMax zero zero    (suc zero)    = refl
+negsuc+negsucnegsuc+posMax zero zero    (suc (suc z)) = refl
+negsuc+negsucnegsuc+posMax zero (suc y) zero          = refl
+negsuc+negsucnegsuc+posMax zero (suc y) (suc zero)    = refl
+negsuc+negsucnegsuc+posMax zero (suc y) (suc (suc z)) = refl
+negsuc+negsucnegsuc+posMax (suc x) y z
+  = cong₂ max (sym (predℤ+ (negsuc x) (negsuc y)))
+              (sym (predℤ+ (negsuc x) (pos z))) ∙
+    sym (predDistMax (negsuc x + negsuc y) (negsuc x + pos z)) ∙
+    cong predℤ (negsuc+negsucnegsuc+posMax x y z) ∙
+    predℤ+ (negsuc x) (pos z)
+
++DistRMin : ∀ x y z → x + min y z ≡ min (x + y) (x + z)
++DistRMin (pos zero) y z = +IdL _ ∙ cong₂ min (pos0+ y) (pos0+ z)
++DistRMin (pos (suc x)) (pos zero) (pos zero)
+  = +IdR _ ∙∙ sym (minIdem (pos (suc x))) ∙∙ cong₂ min (sym $ +IdR _) (sym $ +IdR _)
++DistRMin (pos (suc x)) (pos zero) (pos (suc z))
+  = +IdR _ ∙∙ sym (pos+posRposMin _ _) ∙∙ cong (flip min _) (sym $ +IdR _)
++DistRMin (pos (suc x)) (pos (suc y)) (pos zero)
+  = +IdR _ ∙∙ sym (pos+posLposMin _ _) ∙∙ cong (min _) (sym $ +IdR _)
++DistRMin (pos (suc x)) (pos (suc y)) (pos (suc z))
+  = cong ((pos (suc x) +_) ∘ pos) minSuc ∙
+    (cong pos $ +-suc _ (ℕ.min y z)) ∙
+    (cong (sucℤ ∘ sucℤ) $ +DistRMin (pos x) (pos y) (pos z)) ∙
+    sym (cong (sucℤ ∘ pos) minSuc) ∙ sym (cong pos minSuc) ∙
+    sym (cong₂ (λ p q → min (pos p) (pos q)) (+-suc (suc x) y) (+-suc (suc x) z))
++DistRMin (pos (suc x)) (pos y) (negsuc z)
+  = cong (pos (suc x) +_) (minComm (pos y) (negsuc z)) ∙
+    sym (pos+pospos+negsucMin (suc x) y z)
++DistRMin (pos (suc x)) (negsuc y) (pos z)
+  = sym (minComm _ _ ∙ pos+pospos+negsucMin (suc x) z y)
++DistRMin (pos (suc x)) (negsuc zero) (negsuc zero) = sym (minIdem _)
++DistRMin (pos (suc zero)) (negsuc zero) (negsuc (suc zero)) = refl
++DistRMin (pos (suc zero)) (negsuc zero) (negsuc (suc (suc z))) = refl
++DistRMin (pos (suc (suc x))) (negsuc zero) (negsuc (suc z))
+  = sym (pos+pospos+negsucMin (suc x) 0 z) ∙ cong (flip min _) (+IdR _)
++DistRMin (pos (suc zero)) (negsuc (suc y)) (negsuc zero) = refl
++DistRMin (pos (suc (suc x))) (negsuc (suc y)) (negsuc zero)
+  = sym (pos+pospos+negsucMin (suc x) 0 y) ∙ cong (flip min _) (+IdR _) ∙ minComm _ _
++DistRMin (pos (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (sucℤ+ (pos x) (min (negsuc (suc y)) (negsuc (suc z)))) ∙
+    +sucℤ (pos x) (min (negsuc (suc y)) (negsuc (suc z))) ∙
+    cong (pos x +_) (sucDistMin (negsuc (suc y)) (negsuc (suc z))) ∙
+    +DistRMin (pos x) (negsuc y) (negsuc z)
++DistRMin (negsuc x) (pos zero) (pos zero) = sym (minIdem (negsuc x))
++DistRMin (negsuc x) (pos zero) (pos (suc z)) = sym (negsuc+posRnegsucMin x (suc z))
++DistRMin (negsuc x) (pos (suc y)) (pos zero) = sym (negsuc+posLnegsucMin x (suc y))
++DistRMin (negsuc zero) (pos (suc zero)) (pos (suc zero)) = refl
++DistRMin (negsuc zero) (pos (suc zero)) (pos (suc (suc z))) = refl
++DistRMin (negsuc zero) (pos (suc (suc y))) (pos (suc zero)) = refl
++DistRMin (negsuc zero) (pos (suc (suc y))) (pos (suc (suc z)))
+  = cong (_ℕ- 1) (minSuc {suc y} {suc z}) ∙
+    cong ((_ℕ- 1) ∘ suc) (minSuc {y} {z}) ∙ sym (cong pos minSuc)
++DistRMin (negsuc (suc x)) (pos (suc y)) (pos (suc z))
+  = cong ((negsuc (suc x) +_) ∘ pos) (minSuc {y} {z}) ∙
+    sym (+sucℤ (negsuc (suc x)) (min (pos y) (pos z))) ∙
+    cong sucℤ (+DistRMin (negsuc (suc x)) (pos y) (pos z)) ∙
+    sucDistMin (negsuc (suc x) + pos y) (negsuc (suc x) + pos z) ∙
+    cong₂ min (sucℕ-suc≡ℕ- y (suc x)) (sucℕ-suc≡ℕ- z (suc x))
++DistRMin (negsuc x) (pos y) (negsuc z)
+  = cong (negsuc x +_) (minComm (pos y) (negsuc z)) ∙
+    sym (negsuc+negsucnegsuc+posMin x z y) ∙
+    minComm (negsuc x + negsuc z) (negsuc x + pos y)
++DistRMin (negsuc x) (negsuc y) (pos z) = sym (negsuc+negsucnegsuc+posMin x y z)
++DistRMin (negsuc zero) (negsuc zero) (negsuc zero) = refl
++DistRMin (negsuc zero) (negsuc zero) (negsuc (suc z)) = refl
++DistRMin (negsuc zero) (negsuc (suc y)) (negsuc zero) = refl
++DistRMin (negsuc zero) (negsuc (suc y)) (negsuc (suc z)) = cong negsuc (sym maxSuc)
++DistRMin (negsuc (suc x)) (negsuc zero) (negsuc zero) = sym (minIdem _)
++DistRMin (negsuc (suc x)) (negsuc zero) (negsuc (suc z))
+  = cong -_ (
+    sym (pos+posRposMax ((suc ∘ suc ∘ suc) x) (suc z)) ∙
+    cong pos (maxSuc ∙ cong (suc ∘ flip ℕ.max (suc (suc (x +ℕ suc z))))
+                            (sym (+-zero _))))
++DistRMin (negsuc (suc x)) (negsuc (suc y)) (negsuc zero)
+  = cong negsuc (+-suc _ y) ∙
+    sym (cong predℤ (negsuc+negsucLnegsucMin (suc x) y)) ∙
+    predDistMin (negsuc (suc x) + negsuc y) (negsuc (suc x)) ∙
+    sym (cong₂ (λ p q → min (negsuc p) (negsuc q))
+    (+-suc _ y) (+-zero (suc (suc x))))
++DistRMin (negsuc (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = cong ((negsuc (suc x) +_) ∘ negsuc) maxSuc ∙
+    sym (+predℤ (negsuc (suc x)) (min (negsuc y) (negsuc z))) ∙
+    cong predℤ (+DistRMin (negsuc (suc x)) (negsuc y) (negsuc z)) ∙
+    predDistMin (negsuc (suc x) + negsuc y) (negsuc (suc x) + negsuc z) ∙
+    sym (cong₂ (λ p q → min (negsuc p) (negsuc q)) (+-suc _ y) (+-suc _ z))
+
++DistLMin : ∀ x y z → min x y + z ≡ min (x + z) (y + z)
++DistLMin x y z
+  = +Comm (min x y) z ∙
+    +DistRMin z x y ∙
+    cong₂ min (+Comm z x)
+              (+Comm z y)
+
++DistRMax : ∀ x y z → x + max y z ≡ max (x + y) (x + z)
++DistRMax x y z
+  = sym (-Involutive (x + max y z)) ∙
+    cong -_ (-Dist+ x (max y z) ∙
+             cong (- x +_) (-DistMax y z) ∙
+                  +DistRMin (- x) (- y) (- z)) ∙
+             -DistMin (- x - y) (- x - z) ∙
+    cong₂ max (-Dist+ (- x) (- y) ∙
+               cong₂ _+_ (-Involutive x)
+                         (-Involutive y))
+              (-Dist+ (- x) (- z) ∙
+               cong₂ _+_ (-Involutive x)
+                         (-Involutive z))
+
++DistLMax : ∀ x y z → max x y + z ≡ max (x + z) (y + z)
++DistLMax x y z
+  = +Comm (max x y) z ∙
+    +DistRMax z x y ∙
+    cong₂ max (+Comm z x)
+              (+Comm z y)
+
+pos·pos : (n m : ℕ) → pos (n ·ℕ m) ≡ pos n · pos m
+pos·pos n m = refl
+
+pos·negsuc : (n m : ℕ) → pos n · negsuc m ≡ - (pos n · pos (suc m))
+pos·negsuc zero    m = refl
+pos·negsuc (suc n) m = refl
+
+negsuc·pos : (n m : ℕ) → negsuc n · pos m ≡ - (pos (suc n) · pos m)
+negsuc·pos n zero    = cong (-_ ∘ pos) (ℕ.0≡m·0 n)
+negsuc·pos n (suc m) = refl
+
+negsuc·negsuc : (n m : ℕ) → negsuc n · negsuc m ≡ pos (suc n) · pos (suc m)
+negsuc·negsuc n m = refl
+
+negsuc·ℤ : (n : ℕ) → (m : ℤ) → negsuc n · m ≡ - (pos (suc n) · m)
+negsuc·ℤ n (pos m)    = negsuc·pos n m
+negsuc·ℤ n (negsuc m) = refl
+
+·Comm : (x y : ℤ) → x · y ≡ y · x
+·Comm (pos m)       (pos n)       = cong pos (ℕ.·-comm m n)
+·Comm (pos zero)    (negsuc n)    = refl
+·Comm (pos (suc m)) (negsuc n)    = cong neg $ ℕ.·-comm (suc m) (suc n)
+·Comm (negsuc m)    (pos zero)    = refl
+·Comm (negsuc m)    (pos (suc n)) = cong neg $ ℕ.·-comm (suc m) (suc n)
+·Comm (negsuc m)    (negsuc n)    = cong pos $ ℕ.·-comm (suc m) (suc n)
+
+·IdR : (x : ℤ) → x · 1 ≡ x
+·IdR (pos n)    = cong pos (ℕ.·-identityʳ n)
+·IdR (negsuc n) = cong negsuc (ℕ.·-identityʳ n)
+
+·IdL : (x : ℤ) → 1 · x ≡ x
+·IdL (pos n)    = cong pos (ℕ.+-zero n)
+·IdL (negsuc n) = cong negsuc (ℕ.+-zero n)
+
+·AnnihilR : (x : ℤ) → x · 0 ≡ 0
+·AnnihilR (pos n)    = cong pos $ sym $ ℕ.0≡m·0 n
+·AnnihilR (negsuc n) = refl
+
+·AnnihilL : (x : ℤ) → 0 · x ≡ 0
+·AnnihilL (pos n)    = refl
+·AnnihilL (negsuc n) = refl
+
+-1·x≡-x : ∀ x → -1 · x ≡ - x
+-1·x≡-x (pos zero)    = refl
+-1·x≡-x (pos (suc n)) = cong negsuc (+-zero n)
+-1·x≡-x (negsuc n)    = cong (pos ∘ suc) (+-zero n)
+
+private
+  distrHelper : (x y z w : ℤ) → (x + y) + (z + w) ≡ ((x + z) + (y + w))
+  distrHelper x y z w =
+      +Assoc (x + y) z w
+   ∙∙ cong (_+ w) (sym (+Assoc x y z) ∙∙ cong (x +_) (+Comm y z) ∙∙ +Assoc x z y)
+   ∙∙ sym (+Assoc (x + z) y w)
+
+ℕ-Cancel+ : ∀ m n l → (m +ℕ n) ℕ- (m +ℕ l) ≡ n ℕ- l
+ℕ-Cancel+ zero    n l = refl
+ℕ-Cancel+ (suc m) n l = ℕ-Cancel+ m n l
+
+Pos·DistRℕ- : ∀ x y z → pos x · y ℕ- z ≡ (x ·ℕ y ) ℕ- (x ·ℕ z)
+Pos·DistRℕ- zero y z = ·AnnihilL (y ℕ- z)
+Pos·DistRℕ- (suc x) zero zero =
+  pos (x ·ℕ zero)            ≡⟨ cong pos $ sym $ ℕ.0≡m·0 x ⟩
+  pos 0                      ≡⟨ cong₂ _ℕ-_ (ℕ.0≡m·0 x) (ℕ.0≡m·0 x) ⟩
+  (x ·ℕ zero) ℕ- (x ·ℕ zero) ∎
+Pos·DistRℕ- (suc x) zero    (suc z) = cong (_ℕ- (suc x ·ℕ suc z)) (ℕ.0≡m·0 x)
+Pos·DistRℕ- (suc x) (suc y) zero    = cong ((suc x ·ℕ suc y) ℕ-_) (ℕ.0≡m·0 x)
+Pos·DistRℕ- (suc x) (suc y) (suc z) =
+  pos (suc x) · (y ℕ- z)                         ≡⟨ Pos·DistRℕ- (suc x) y z ⟩
+  (suc x ·ℕ y) ℕ- (suc x ·ℕ z)                   ≡⟨ sym $ ℕ-Cancel+ (suc x) (suc x ·ℕ y) (suc x ·ℕ z) ⟩
+  (suc x +ℕ suc x ·ℕ y) ℕ- (suc x +ℕ suc x ·ℕ z) ≡⟨ sym $ cong₂ _ℕ-_ (ℕ.·-suc (suc x) y) (ℕ.·-suc (suc x) z) ⟩
+  (suc x ·ℕ suc y) ℕ- (suc x ·ℕ suc z)           ∎
+
+Negsuc·DistRℕ- : ∀ x y z → negsuc x · y ℕ- z ≡ (suc x ·ℕ suc z) ℕ- (suc x ·ℕ suc y)
+Negsuc·DistRℕ- m n l =
+  negsuc m · (suc n ℕ- suc l)                  ≡⟨ negsuc·ℤ m (n ℕ- l) ⟩
+  - (pos (suc m) · (suc n ℕ- suc l))           ≡⟨ cong -_ (Pos·DistRℕ- (suc m) (suc n) (suc l)) ⟩
+  - ((suc m ·ℕ suc n) ℕ- (suc m ·ℕ suc l))     ≡⟨ sym $ ℕ-AntiComm (suc m ·ℕ suc l) (suc m ·ℕ suc n) ⟩
+  negsuc m · pos (suc n) + negsuc m · negsuc l ∎
+
+·DistR+ : (x y z : ℤ) → x · (y + z) ≡ x · y + x · z
+·DistR+ (pos m)       (pos n)    (pos l)    = cong pos $ sym $ ℕ.·-distribˡ m n l
+·DistR+ (pos zero)    (pos n)    (negsuc l) = ·AnnihilL (n ℕ- suc l)
+·DistR+ (pos (suc m)) (pos n)    (negsuc l) = Pos·DistRℕ- (suc m) n (suc l)
+·DistR+ (pos zero)    (negsuc n) (pos l)    = ·AnnihilL (l ℕ- suc n)
+·DistR+ (pos (suc m)) (negsuc n) (pos l)    = Pos·DistRℕ- (suc m) l (suc n)
+·DistR+ (pos zero)    (negsuc n) (negsuc l) = refl
+·DistR+ (pos (suc m)) (negsuc n) (negsuc l) = cong neg $
+  suc m ·ℕ suc (suc (n +ℕ l))               ≡⟨ cong (suc m ·ℕ_) (sym (ℕ.+-suc (suc n) l)) ⟩
+  suc m ·ℕ (suc n +ℕ suc l)                 ≡⟨ sym (ℕ.·-distribˡ (suc m) (suc n) (suc l)) ⟩
+  suc m ·ℕ suc n +ℕ suc m ·ℕ suc l          ≡⟨⟩
+  suc m ·ℕ suc n +ℕ suc (l +ℕ m ·ℕ suc l)   ≡⟨ ℕ.+-suc (suc m ·ℕ suc n) (l +ℕ m ·ℕ suc l) ⟩
+  suc (suc m ·ℕ suc n) +ℕ (l +ℕ m ·ℕ suc l) ∎
+·DistR+ (negsuc m) (pos zero)    (pos zero)    = refl
+·DistR+ (negsuc m) (pos zero)    (pos (suc l)) = refl
+·DistR+ (negsuc m) (pos (suc n)) (pos zero)    = λ i → negsuc $ (ℕ.+-zero n i) +ℕ m ·ℕ suc (ℕ.+-zero n i)
+·DistR+ (negsuc m) (pos (suc n)) (pos (suc l)) = cong neg $
+  suc m ·ℕ suc (n +ℕ suc l)                      ≡⟨ (sym $ ℕ.·-distribˡ (suc m) (suc n) (suc l) ) ⟩
+  suc m ·ℕ suc n +ℕ suc m ·ℕ suc l               ≡⟨⟩
+  suc n +ℕ m ·ℕ suc n +ℕ suc (l +ℕ m ·ℕ suc l)   ≡⟨ ℕ.+-suc ((suc n) +ℕ m ·ℕ suc n) (l +ℕ m ·ℕ suc l)  ⟩
+  suc (suc n) +ℕ m ·ℕ suc n +ℕ (l +ℕ m ·ℕ suc l) ∎
+·DistR+ (negsuc m) (pos zero)    (negsuc l)    = refl
+·DistR+ (negsuc m) (pos (suc n)) (negsuc l)    = Negsuc·DistRℕ- m n l
+·DistR+ (negsuc m) (negsuc n)    (pos zero)    = cong pos $ sym $ ℕ.+-zero (suc m ·ℕ suc n)
+·DistR+ (negsuc m) (negsuc n)    (pos (suc l)) = Negsuc·DistRℕ- m l n
+·DistR+ (negsuc m) (negsuc n)    (negsuc l)    = cong pos $
+  suc m ·ℕ suc (suc (n +ℕ l))      ≡⟨ cong (suc m ·ℕ_) (sym (ℕ.+-suc (suc n) l)) ⟩
+  suc m ·ℕ (suc n +ℕ suc l)        ≡⟨ sym (ℕ.·-distribˡ (suc m) (suc n) (suc l)) ⟩
+  suc m ·ℕ suc n +ℕ suc m ·ℕ suc l ∎
+
+·DistL+ : (x y z : ℤ) → (x + y) · z ≡ x · z + y · z
+·DistL+ x y z = ·Comm (x + y) z ∙∙ ·DistR+ z x y ∙∙ cong₂ _+_ (·Comm z x) (·Comm z y)
+
+-DistL· : (b c : ℤ) → - (b · c) ≡ - b · c
+-DistL· (pos zero)    (pos n)       = refl
+-DistL· (pos (suc m)) (pos zero)    = cong (-_ ∘ pos) $ sym $ ℕ.0≡m·0 m
+-DistL· (pos (suc m)) (pos (suc n)) = refl
+-DistL· (pos zero)    (negsuc n)    = refl
+-DistL· (pos (suc m)) (negsuc n)    = refl
+-DistL· (negsuc m)    (pos zero)    = cong pos (ℕ.0≡m·0 m)
+-DistL· (negsuc m)    (pos (suc n)) = refl
+-DistL· (negsuc m)    (negsuc n)    = refl
+
+-DistR· : (b c : ℤ) → - (b · c) ≡ b · - c
+-DistR· b c = cong (-_) (·Comm b c) ∙∙ -DistL· c b ∙∙ ·Comm (- c) b
+
+-DistLR· : (b c : ℤ) → b · c ≡ - b · - c
+-DistLR· b c = sym (-Involutive (b · c)) ∙ (λ i → - -DistL· b c i) ∙ -DistR· (- b) c
+
+ℤ·negsuc : (n : ℤ) (m : ℕ) → n · negsuc m ≡ - (n · pos (suc m))
+ℤ·negsuc (pos zero)    zero    = refl
+ℤ·negsuc (pos (suc n)) zero    = refl
+ℤ·negsuc (pos zero)    (suc m) = refl
+ℤ·negsuc (pos (suc n)) (suc m) = refl
+ℤ·negsuc (negsuc n)    zero    = refl
+ℤ·negsuc (negsuc n)    (suc m) = refl
+
+private
+  neg·Assoc : ∀ m n l → negsuc m · (negsuc n · negsuc l) ≡ (negsuc m · negsuc n) · negsuc l
+  neg·Assoc m n l = cong neg (ℕ.·-assoc (suc m) (suc n) (suc l))
+  pos·Assoc : ∀ m n l → pos m · (pos n · pos l) ≡ (pos m · pos n) · pos l
+  pos·Assoc m n l = cong pos (ℕ.·-assoc m n l)
+
+·Assoc : (a b c : ℤ) → (a · (b · c)) ≡ ((a · b) · c)
+·Assoc (pos m)       (pos n)       (pos l)       = pos·Assoc m n l
+·Assoc (pos m)       (pos (zero))  (negsuc l)    =
+  pos (suc m ·ℕ 0)           ≡⟨ cong pos $ sym $ ℕ.0≡m·0 m ⟩
+  0                          ≡⟨ sym $ ·AnnihilL (negsuc l) ⟩
+  0 · negsuc l               ≡⟨ cong (_· negsuc l) (cong pos (ℕ.0≡m·0 m)) ⟩
+  pos (m ·ℕ zero) · negsuc l ∎
+·Assoc (pos zero)    (pos (suc n)) (negsuc l)    = refl
+·Assoc (pos (suc m)) (pos (suc n)) (negsuc l)    = neg·Assoc m n l
+·Assoc (pos zero)    (negsuc n)    (pos zero)    = refl
+·Assoc (pos zero)    (negsuc n)    (pos (suc l)) = refl
+·Assoc (pos (suc m)) (negsuc n)    (pos zero)    = cong pos $ sym $ ℕ.0≡m·0 m
+·Assoc (pos (suc m)) (negsuc n)    (pos (suc l)) = neg·Assoc m n l
+·Assoc (pos zero)    (negsuc n)    (negsuc l)    = refl
+·Assoc (pos (suc m)) (negsuc n)    (negsuc l)    = pos·Assoc (suc m) (suc n) (suc l)
+·Assoc (negsuc m)    (pos zero)    (pos l)       = refl
+·Assoc (negsuc m)    (pos (suc n)) (pos zero)    =
+  negsuc m · pos (n ·ℕ 0) ≡⟨ cong ((negsuc m ·_) ∘ pos) $ sym $ ℕ.0≡m·0 n ⟩
+  negsuc m · 0            ≡⟨ ·AnnihilR (negsuc m) ⟩
+  0                       ∎
+·Assoc (negsuc m)    (pos (suc n)) (pos (suc l)) = neg·Assoc m n l
+·Assoc (negsuc m)    (pos zero)    (negsuc l)    = refl
+·Assoc (negsuc m)    (pos (suc n)) (negsuc l)    = pos·Assoc (suc m) (suc n) (suc l)
+·Assoc (negsuc m)    (negsuc n)    (pos zero)    = cong pos $ ℕ.0≡m·0 (suc m ·ℕ suc n)
+·Assoc (negsuc m)    (negsuc n)    (pos (suc l)) = pos·Assoc (suc m) (suc n) (suc l)
+·Assoc (negsuc m)    (negsuc n)    (negsuc l)    = neg·Assoc m n l
+
+·suc→0 : (a : ℤ) (b : ℕ) → a · pos (suc b) ≡ 0 → a ≡ 0
+·suc→0 (pos n) b n·b≡0 = cong pos (sym (0≡n·sm→0≡n (sym (injPos (pos·pos n (suc b) ∙ n·b≡0)))))
+·suc→0 (negsuc n) b n·b≡0 = ⊥.rec (snotz
+                                     (injNeg
+                                      (cong -_ (pos·pos (suc n) (suc b)) ∙
+                                       sym (negsuc·pos n (suc b)) ∙
+                                       n·b≡0)))
+
+sucℤ≡1+ : ∀ a → sucℤ a ≡ 1 + a
+sucℤ≡1+ (pos n)          = refl
+sucℤ≡1+ (negsuc zero)    = refl
+sucℤ≡1+ (negsuc (suc n)) = refl
+
+sucℤ· : (a b : ℤ) → sucℤ a · b ≡ b + a · b
+sucℤ· a b =
+  sucℤ a · b    ≡⟨ cong (_· b) (sucℤ≡1+ a) ⟩
+  (1 + a) · b   ≡⟨ ·DistL+ 1 a b ⟩
+  1 · b + a · b ≡⟨ cong (_+ a · b) (·IdL b) ⟩
+  b + a · b     ∎
+
+·sucℤ : (a b : ℤ) → a · sucℤ b ≡ a · b + a
+·sucℤ a b = ·Comm a (sucℤ b) ∙ sucℤ· b a ∙ cong (a +_) (·Comm b a) ∙ +Comm a (a · b)
+
+predℤ≡-1 : ∀ a → predℤ a ≡ a - 1
+predℤ≡-1 (pos zero)          = refl
+predℤ≡-1 (pos (suc zero))    = refl
+predℤ≡-1 (pos (suc (suc n))) = refl
+predℤ≡-1 (negsuc n)          = cong (negsuc ∘ suc) $ sym $ ℕ.+-zero n
+
+predℤ· : (a  b : ℤ) → predℤ a · b ≡ - b + a · b
+predℤ· a b =
+  predℤ a · b       ≡⟨ cong (_· b) (predℤ≡-1 a) ⟩
+  (a - 1) · b       ≡⟨ cong (_· b) (+Comm a -1) ⟩
+  (-1 + a) · b      ≡⟨ ·DistL+ -1 a b ⟩
+  -1 · b + a · b    ≡⟨ cong (_+ a · b) (negsuc·ℤ 0 b) ⟩
+  - (1 · b) + a · b ≡⟨ cong ((_+ a · b) ∘ -_) (·IdL b) ⟩
+  - b + a · b       ∎
+
+·predℤ : ∀ a b → a · predℤ b ≡ a · b - a
+·predℤ a b = ·Comm a (predℤ b) ∙ predℤ· b a ∙ cong ((- a) +_) (·Comm b a) ∙ +Comm (- a) (a · b)
+
+·DistPosRMin : (x : ℕ) (y z : ℤ) → pos x · min y z ≡ min (pos x · y) (pos x · z)
+·DistPosRMin zero y z = ·AnnihilL _ ∙ sym (cong₂ min (·AnnihilL _) (·AnnihilL _))
+·DistPosRMin (suc x) (pos zero) (pos zero)
+  = ·AnnihilR (pos (suc x)) ∙
+    sym (cong₂ min (·AnnihilR (pos (suc x))) (·AnnihilR (pos (suc x))))
+·DistPosRMin (suc x) (pos zero) (pos (suc z))
+  = ·AnnihilR (pos (suc x)) ∙
+    sym (cong (flip min _) (·AnnihilR (pos (suc x))))
+·DistPosRMin (suc x) (pos (suc y)) (pos zero)
+  = ·AnnihilR (pos (suc x)) ∙
+    sym (cong₂ min (·Comm (pos (suc x)) (pos (suc y))) (·AnnihilR (pos (suc x))))
+·DistPosRMin (suc x) (pos (suc y)) (pos (suc z))
+  = cong (pos ∘ (suc x ·ℕ_)) minSuc ∙
+    ·sucℤ (pos (suc x)) (min (pos y) (pos z)) ∙
+    cong (_+ pos (suc x)) (·DistPosRMin (suc x) (pos y) (pos z)) ∙
+    +DistLMin (pos (suc x) · pos y) (pos (suc x) · pos z) (pos (suc x)) ∙
+    cong₂ min (sym (·sucℤ (pos (suc x)) (pos y)))
+              (sym (·sucℤ (pos (suc x)) (pos z)))
+·DistPosRMin (suc x) (pos y) (negsuc z)
+  = cong (pos (suc x) ·_) (minComm (pos y) (negsuc z)) ∙
+    sym (cong₂ min (sym (pos·pos (suc x) y))
+                   (pos·negsuc (suc x) z ∙
+                    cong -_ (sym (pos·pos (suc x) (suc z)))) ∙
+         min- (suc x ·ℕ y) (suc x ·ℕ suc z) ∙
+         cong -_ (pos·pos (suc x) (suc z)) ∙
+         sym (pos·negsuc (suc x) z))
+·DistPosRMin (suc x) (negsuc y) (pos z)
+  = sym (cong₂ min (pos·negsuc (suc x) y ∙
+                    cong -_ (sym (pos·pos (suc x) (suc y))))
+                   (sym (pos·pos (suc x) z)) ∙
+         -min (suc x ·ℕ suc y) (suc x ·ℕ z) ∙
+         cong -_ (pos·pos (suc x) (suc y)) ∙
+         sym (pos·negsuc (suc x) y))
+·DistPosRMin (suc x) (negsuc zero) (negsuc zero)
+  = sym (minIdem (pos (suc x) · negsuc zero))
+·DistPosRMin (suc x) (negsuc zero) (negsuc (suc z))
+  = ·Comm (pos (suc x)) (negsuc (suc z)) ∙
+    cong negsuc (+-suc x _) ∙
+    sym (negsuc+negsucRnegsucMin x (x +ℕ z ·ℕ suc x)) ∙
+    sym (cong₂ min (cong negsuc (·-identityʳ x))
+                   (·Comm (pos (suc x)) (negsuc (suc z)) ∙
+                     cong negsuc (+-suc x _)))
+·DistPosRMin (suc x) (negsuc (suc y)) (negsuc zero)
+  = ·Comm (pos (suc x)) (negsuc (suc y)) ∙
+    cong negsuc (+-suc x _) ∙
+    sym (negsuc+negsucLnegsucMin x (x +ℕ y ·ℕ suc x)) ∙
+    sym (cong₂ min (·Comm (pos (suc x)) (negsuc (suc y)) ∙ cong negsuc (+-suc x _))
+                   (cong negsuc (·-identityʳ x)))
+·DistPosRMin (suc x) (negsuc (suc y)) (negsuc (suc z))
+  = cong ((pos (suc x) ·_) ∘ negsuc) maxSuc ∙
+    ·predℤ (pos (suc x)) (min (negsuc y) (negsuc z)) ∙
+    cong (_- pos (suc x)) (·DistPosRMin (suc x) (negsuc y) (negsuc z)) ∙
+    +DistLMin (pos (suc x) · negsuc y) (pos (suc x) · negsuc z) (- pos (suc x)) ∙
+    cong₂ min (sym (·predℤ (pos (suc x)) (negsuc y)))
+              (sym (·predℤ (pos (suc x)) (negsuc z)))
+
+·DistPosLMin : (x y : ℤ) (z : ℕ) → min x y · pos z ≡ min (x · pos z) (y · pos z)
+·DistPosLMin y z x = ·Comm (min y z) (pos x) ∙
+                     ·DistPosRMin x y z ∙
+                     cong₂ min (·Comm (pos x) y)
+                               (·Comm (pos x) z)
+
+·DistPosRMax : (x : ℕ) (y z : ℤ) → pos x · max y z ≡ max (pos x · y) (pos x · z)
+·DistPosRMax x y z
+  = sym (-Involutive (pos x · max y z)) ∙
+    cong -_ (-DistR· (pos x) (max y z) ∙
+             cong (pos x ·_) (-DistMax y z) ∙
+             ·DistPosRMin x (- y) (- z)) ∙
+    -DistMin (pos x · - y) (pos x · - z) ∙
+    cong₂ max (-DistR· (pos x) (- y) ∙
+               cong (pos x ·_) (-Involutive y))
+              (-DistR· (pos x) (- z) ∙
+               cong (pos x ·_) (-Involutive z))
+
+·DistPosLMax : (x y : ℤ) (z : ℕ) → max x y · pos z ≡ max (x · pos z) (y · pos z)
+·DistPosLMax y z x = ·Comm (max y z) (pos x) ∙
+                     ·DistPosRMax x y z ∙
+                     cong₂ max (·Comm (pos x) y)
+                               (·Comm (pos x) z)
+
+·DistNegsucRMin : (x : ℕ) (y z : ℤ) → negsuc x · min y z ≡ max (negsuc x · y) (negsuc x · z)
+·DistNegsucRMin x y z
+  = -DistLR· (negsuc x) (min y z) ∙
+    cong (pos (suc x) ·_) (-DistMin y z) ∙
+    ·DistPosRMax (suc x) (- y) (- z) ∙
+    cong₂ max (sym (-DistR· (pos (suc x)) y) ∙
+               -DistL· (pos (suc x)) y)
+              (sym (-DistR· (pos (suc x)) z) ∙
+               -DistL· (pos (suc x)) z)
+
+·DistNegsucLMin : (x y : ℤ) (z : ℕ) → min x y · negsuc z ≡ max (x · negsuc z) (y · negsuc z)
+·DistNegsucLMin y z x = ·Comm (min y z) (negsuc x) ∙
+                        ·DistNegsucRMin x y z ∙
+                        cong₂ max (·Comm (negsuc x) y)
+                                  (·Comm (negsuc x) z)
+
+·DistNegsucRMax : (x : ℕ) (y z : ℤ) → negsuc x · max y z ≡ min (negsuc x · y) (negsuc x · z)
+·DistNegsucRMax x y z
+  = -DistLR· (negsuc x) (max y z) ∙
+    cong (pos (suc x) ·_) (-DistMax y z) ∙
+    ·DistPosRMin (suc x) (- y) (- z) ∙
+    cong₂ min (sym (-DistR· (pos (suc x)) y) ∙
+               -DistL· (pos (suc x)) y)
+              (sym (-DistR· (pos (suc x)) z) ∙
+               -DistL· (pos (suc x)) z)
+
+·DistNegsucLMax : (x y : ℤ) (z : ℕ) → max x y · negsuc z ≡ min (x · negsuc z) (y · negsuc z)
+·DistNegsucLMax y z x = ·Comm (max y z) (negsuc x) ∙
+                        ·DistNegsucRMax x y z ∙
+                        cong₂ min (·Comm (negsuc x) y)
+                                  (·Comm (negsuc x) z)
+
+minus≡0- : (x : ℤ) → - x ≡ (0 - x)
+minus≡0- (pos zero)    = refl
+minus≡0- (pos (suc n)) = refl
+minus≡0- (negsuc n)    = refl
+
+absPos·Pos : (m n : ℕ) → abs (pos m · pos n) ≡ abs (pos m) ·ℕ abs (pos n)
+absPos·Pos m n = refl
+
+abs· : (m n : ℤ) → abs (m · n) ≡ abs m ·ℕ abs n
+abs· (pos m)       (pos n)       = refl
+abs· (pos zero)    (negsuc n)    = refl
+abs· (pos (suc m)) (negsuc n)    = refl
+abs· (negsuc m)    (pos zero)    = 0≡m·0 m
+abs· (negsuc m)    (pos (suc n)) = refl
+abs· (negsuc m)    (negsuc n)    = refl
+
+sign·abs : ∀ m → sign m · pos (abs m) ≡ m
+sign·abs (pos zero)    = refl
+sign·abs (pos (suc n)) = cong (pos ∘ suc) (ℕ.+-zero n)
+sign·abs (negsuc n)    = cong negsuc (ℕ.+-zero n)
+
+-- ℤ is integral domain
+
+isIntegralℤPosPos : (c m : ℕ) → pos c · pos m ≡ 0 → ¬ c ≡ 0 → m ≡ 0
+isIntegralℤPosPos zero    m p c≠0 =  ⊥.rec (c≠0 refl)
+isIntegralℤPosPos (suc c) m p _   = sym $ ℕ.0≡n·sm→0≡n $ injPos $
+  pos 0               ≡⟨ sym p ⟩
+  pos (suc c) · pos m ≡⟨ ·Comm (pos (suc c)) (pos m)  ⟩
+  pos m · pos (suc c) ∎
+
+isIntegralℤ : (c m : ℤ) → c · m ≡ 0 → ¬ c ≡ 0 → m ≡ 0
+isIntegralℤ (pos zero)    (pos m)       p h = ⊥.rec (h refl)
+isIntegralℤ (pos (suc c)) (pos m)       p h = cong pos (isIntegralℤPosPos (suc c) m p ℕ.snotz)
+isIntegralℤ (pos zero)    (negsuc m)    p h = ⊥.rec (h refl)
+isIntegralℤ (pos (suc c)) (negsuc m)    p h = ⊥.rec (negsucNotpos (predℕ (suc c ·ℕ suc m)) 0 p )
+isIntegralℤ (negsuc c)    (pos zero)    p h = refl
+isIntegralℤ (negsuc c)    (pos (suc m)) p h = ⊥.rec (negsucNotpos (predℕ (suc c ·ℕ suc m)) 0 p )
+isIntegralℤ (negsuc c)    (negsuc m)    p h = ⊥.rec (ℕ.snotz (injPos p))
+
+private
+  ·lCancel-helper : (c m n : ℤ) → c · m ≡ c · n → c · (m - n) ≡ 0
+  ·lCancel-helper c m n p =
+      ·DistR+ c m (- n)
+    ∙ (λ i → c · m + -DistR· c n (~ i))
+    ∙ subst (λ a → c · m - a ≡ 0) p (-Cancel (c · m))
+
+·lCancel : (c m n : ℤ) → c · m ≡ c · n → ¬ c ≡ 0 → m ≡ n
+·lCancel c m n p h = -≡0 _ _ (isIntegralℤ c (m - n) (·lCancel-helper c m n p) h)
+
+·rCancel : (c m n : ℤ) → m · c ≡ n · c → ¬ c ≡ 0 → m ≡ n
+·rCancel c m n p h = ·lCancel c m n (·Comm c m ∙ p ∙ ·Comm n c) h
+
+-Cancel'' : ∀ z → z ≡ - z → z ≡ 0
+-Cancel'' z r = isIntegralℤ 2 z (
+    2 · z         ≡⟨ ·DistL+ 1 1 z ⟩
+    1 · z + 1 · z ≡⟨ cong₂ _+_ (·IdL z) (·IdL z) ⟩
+    z + z         ≡⟨ cong (z +_) r ⟩
+    z + - z       ≡⟨ -Cancel z ⟩
+    0             ∎)
+  λ r → ⊥.rec (snotz (injPos r))
+
+-- some lemmas about finite sums
+
+sumFinℤ0 : (n : ℕ) → sumFinℤ {n = n} (λ (x : Fin n) → 0) ≡ 0
+sumFinℤ0 n = sumFinGen0 _+_ 0 +IdR n (λ _ → 0) λ _ → refl
+
+sumFinℤHom : {n : ℕ} (f g : Fin n → ℤ)
+  → sumFinℤ {n = n} (λ x → f x + g x) ≡ sumFinℤ {n = n} f + sumFinℤ {n = n} g
+sumFinℤHom {n = n} = sumFinGenHom _+_ 0 +IdR +Comm +Assoc n
diff --git a/Cubical/Data/Int/Base.agda b/Cubical/Data/Int/Base.agda
index 5dd11a5c6a..69fa38f587 100644
--- a/Cubical/Data/Int/Base.agda
+++ b/Cubical/Data/Int/Base.agda
@@ -42,6 +42,11 @@ abs : ℤ → ℕ
 abs (pos n) = n
 abs (negsuc n) = suc n
 
+sign : ℤ → ℤ
+sign (pos zero) = pos zero
+sign (pos (suc n)) = pos (suc zero)
+sign (negsuc n) = negsuc zero
+
 _ℕ-_ : ℕ → ℕ → ℤ
 a ℕ- 0 = pos a
 0 ℕ- suc b = negsuc b
diff --git a/Cubical/Data/Int/Fast/Base.agda b/Cubical/Data/Int/Fast/Base.agda
deleted file mode 100644
index f5a4ad1bcb..0000000000
--- a/Cubical/Data/Int/Fast/Base.agda
+++ /dev/null
@@ -1,32 +0,0 @@
-module Cubical.Data.Int.Fast.Base where
-
-open import Cubical.Foundations.Prelude
-open import Cubical.Data.Nat as ℕ hiding (_+_ ; _·_)
-open import Cubical.Data.Int.Base hiding (_ℕ-_ ; _+_ ; _-_ ; _·_) public
-
-infixl 7 _·_
-infixl 6 _+_ _-_
-
-ℕ-hlp : ℕ → ℕ → ℤ
-ℕ-hlp m-n@zero n-m = - (pos n-m)
-ℕ-hlp m-n@(suc _) n-m = pos m-n
-
-_ℕ-_ : ℕ → ℕ → ℤ
-m ℕ- n = ℕ-hlp (m ℕ.∸ n) (n ℕ.∸ m)
-
-_+_ : ℤ → ℤ → ℤ
-pos n + pos n₁ = pos (n ℕ.+ n₁)
-negsuc n + negsuc n₁ = negsuc (suc (n ℕ.+ n₁))
-pos n + negsuc n₁ = n ℕ- (suc n₁)
-negsuc n + pos n₁ = n₁ ℕ- (suc n)
-
-_-_ : ℤ → ℤ → ℤ
-m - n = m + (- n)
-
-_·_ : ℤ → ℤ → ℤ
-pos n · pos n₁ = pos (n ℕ.· n₁)
-pos zero · negsuc n₁ = pos zero
-pos (suc n) · negsuc n₁ = negsuc (predℕ (suc n ℕ.· suc n₁))
-negsuc n · pos zero = pos zero
-negsuc n · pos (suc n₁) = negsuc (predℕ (suc n ℕ.· suc n₁))
-negsuc n · negsuc n₁ = pos (suc n ℕ.· suc n₁)
diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda
index f345fdfab9..cdea86ea9d 100644
--- a/Cubical/Data/Int/Properties.agda
+++ b/Cubical/Data/Int/Properties.agda
@@ -1454,6 +1454,11 @@ abs· (negsuc m) (pos n) =
   cong abs (negsuc·pos m n) ∙ abs- (pos (suc m) · pos n) ∙ absPos·Pos (suc m) n
 abs· (negsuc m) (negsuc n) = cong abs (negsuc·negsuc m n) ∙ absPos·Pos (suc m) (suc n)
 
+sign·abs : ∀ m → sign m · pos (abs m) ≡ m
+sign·abs (pos zero) = refl
+sign·abs (pos (suc n)) = refl
+sign·abs (negsuc n) = refl
+
 -- ℤ is integral domain
 
 isIntegralℤPosPos : (c m : ℕ) → pos c · pos m ≡ 0 → ¬ c ≡ 0 → m ≡ 0
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 1c703c358c..633e3bf75c 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -45,6 +45,11 @@ compPropRel R S .snd _ _ = squash₁
 graphRel : ∀ {ℓ} {A B : Type ℓ} → (A → B) → Rel A B ℓ
 graphRel f a b = f a ≡ b
 
+data Ordering : Type where
+  LT : Ordering
+  EQ : Ordering
+  GT : Ordering
+
 module HeterogenousRelation {ℓ ℓ' : Level} {A B : Type ℓ} (R : Rel A B ℓ') where
   isUniversalRel : Type (ℓ-max ℓ ℓ')
   isUniversalRel = (a : A) (b : B) → R a b
diff --git a/Cubical/Relation/Binary/Order/Loset/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Loset/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..4c4b496b59
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Loset/Instances/Fast/Int.agda
@@ -0,0 +1,40 @@
+module Cubical.Relation.Binary.Order.Loset.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sum
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Empty as ⊥
+
+open import Cubical.Data.Fast.Int
+open import Cubical.Data.Fast.Int.Order renaming (_<_ to _<ℤ_)
+
+open import Cubical.Relation.Binary.Order.Loset
+
+open import Cubical.Relation.Binary
+open BinaryRelation
+
+open LosetStr
+
+ℤ<Loset : Loset ℓ-zero ℓ-zero
+fst ℤ<Loset = ℤ
+_<_ (snd ℤ<Loset) = _<ℤ_
+isLoset (snd ℤ<Loset) = isLosetℤ<
+  where
+    open IsLoset
+    abstract
+      isLosetℤ< : IsLoset _<ℤ_
+      isLosetℤ< .is-set         = isSetℤ
+      isLosetℤ< .is-prop-valued = λ _ _ → isProp<
+      isLosetℤ< .is-irrefl      = λ _ → isIrrefl<
+      isLosetℤ< .is-trans       = λ _ _ _ → isTrans<
+      isLosetℤ< .is-asym        = λ _ _ a<b b<a → isIrrefl< (isTrans< a<b b<a)
+      isLosetℤ< .is-weakly-linear a b c a<b with a ≟ c
+      ... | lt a<c = ∣ inl a<c ∣₁
+      ... | eq a≡c = ∣ inr (recompute< (subst (_<ℤ b) a≡c a<b)) ∣₁
+      ... | gt c<a = ∣ inr (isTrans< c<a a<b) ∣₁
+      isLosetℤ< .is-connected a b (¬a<b , ¬b<a) with a ≟ b
+      ... | lt a<b = ⊥.rec (¬a<b a<b)
+      ... | eq a≡b = a≡b
+      ... | gt b<a = ⊥.rec (¬b<a b<a)
diff --git a/Cubical/Relation/Binary/Order/Poset/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Poset/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..d6aebf5967
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Poset/Instances/Fast/Int.agda
@@ -0,0 +1,11 @@
+module Cubical.Relation.Binary.Order.Poset.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Toset
+
+open import Cubical.Relation.Binary.Order.Toset.Instances.Fast.Int
+
+ℤ≤Poset : Poset ℓ-zero ℓ-zero
+ℤ≤Poset = Toset→Poset ℤ≤Toset
diff --git a/Cubical/Relation/Binary/Order/Proset/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Proset/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..d102dcb2da
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Proset/Instances/Fast/Int.agda
@@ -0,0 +1,11 @@
+module Cubical.Relation.Binary.Order.Proset.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Order.Poset
+open import Cubical.Relation.Binary.Order.Proset
+
+open import Cubical.Relation.Binary.Order.Poset.Instances.Fast.Int
+
+ℤ≤Proset : Proset ℓ-zero ℓ-zero
+ℤ≤Proset = Poset→Proset ℤ≤Poset
diff --git a/Cubical/Relation/Binary/Order/Pseudolattice/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Pseudolattice/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..8d23e65e87
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Pseudolattice/Instances/Fast/Int.agda
@@ -0,0 +1,18 @@
+module Cubical.Relation.Binary.Order.Pseudolattice.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Fast.Int
+open import Cubical.Data.Fast.Int.Order renaming (_≤_ to _≤ℤ_)
+
+open import Cubical.Relation.Binary.Order.Poset.Instances.Fast.Int
+open import Cubical.Relation.Binary.Order.Pseudolattice
+
+ℤ≤Pseudolattice : Pseudolattice ℓ-zero ℓ-zero
+ℤ≤Pseudolattice = makePseudolatticeFromPoset ℤ≤Poset min max
+  min≤
+  (recompute≤ (subst (_≤ℤ _) (minComm _ _) min≤))
+  (λ x≤a x≤b → recompute≤ (subst (_≤ℤ min _ _) (minIdem _) (≤MonotoneMin x≤a x≤b)))
+  ≤max
+  (recompute≤ (subst (_ ≤ℤ_) (maxComm _ _) ≤max))
+  (λ a≤x b≤x → recompute≤ (subst (max _ _ ≤ℤ_) (maxIdem _) (≤MonotoneMax a≤x b≤x)))
diff --git a/Cubical/Relation/Binary/Order/Quoset/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Quoset/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..0117b48560
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Quoset/Instances/Fast/Int.agda
@@ -0,0 +1,11 @@
+module Cubical.Relation.Binary.Order.Quoset.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Order.Quoset
+open import Cubical.Relation.Binary.Order.StrictOrder
+
+open import Cubical.Relation.Binary.Order.StrictOrder.Instances.Fast.Int
+
+ℤ<Quoset : Quoset ℓ-zero ℓ-zero
+ℤ<Quoset = StrictOrder→Quoset ℤ<StrictOrder
diff --git a/Cubical/Relation/Binary/Order/StrictOrder/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/StrictOrder/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..60c17cc2c9
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/StrictOrder/Instances/Fast/Int.agda
@@ -0,0 +1,11 @@
+module Cubical.Relation.Binary.Order.StrictOrder.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Relation.Binary.Order.StrictOrder
+open import Cubical.Relation.Binary.Order.Loset
+
+open import Cubical.Relation.Binary.Order.Loset.Instances.Fast.Int
+
+ℤ<StrictOrder : StrictOrder ℓ-zero ℓ-zero
+ℤ<StrictOrder = Loset→StrictOrder ℤ<Loset
diff --git a/Cubical/Relation/Binary/Order/Toset/Instances/Fast/Int.agda b/Cubical/Relation/Binary/Order/Toset/Instances/Fast/Int.agda
new file mode 100644
index 0000000000..06de4c0cea
--- /dev/null
+++ b/Cubical/Relation/Binary/Order/Toset/Instances/Fast/Int.agda
@@ -0,0 +1,34 @@
+module Cubical.Relation.Binary.Order.Toset.Instances.Fast.Int where
+
+open import Cubical.Foundations.Prelude
+
+open import Cubical.Data.Sum
+open import Cubical.HITs.PropositionalTruncation
+
+open import Cubical.Data.Fast.Int
+open import Cubical.Data.Fast.Int.Order renaming (_≤_ to _≤ℤ_)
+
+open import Cubical.Relation.Binary.Order.Toset
+
+open import Cubical.Relation.Binary
+open BinaryRelation
+
+open TosetStr
+
+ℤ≤Toset : Toset ℓ-zero ℓ-zero
+fst ℤ≤Toset = ℤ
+_≤_ (snd ℤ≤Toset) = _≤ℤ_
+isToset (snd ℤ≤Toset) = isTosetℤ≤
+  where
+    open IsToset
+    abstract
+      isTosetℤ≤ : IsToset _≤ℤ_
+      isTosetℤ≤ .is-set         = isSetℤ
+      isTosetℤ≤ .is-prop-valued = λ _ _ → isProp≤
+      isTosetℤ≤ .is-refl        = λ _ → isRefl≤
+      isTosetℤ≤ .is-trans       = λ _ _ _ → isTrans≤
+      isTosetℤ≤ .is-antisym     = λ _ _ → isAntisym≤
+      isTosetℤ≤ .is-total a b with a ≟ b
+      ... | lt a<b = ∣ inl (<-weaken a<b) ∣₁
+      ... | eq a≡b = ∣ inl (recompute≤ (subst (a ≤ℤ_) a≡b isRefl≤)) ∣₁
+      ... | gt b<a = ∣ inr (<-weaken b<a) ∣₁