From c703c36de9766fddb29e26aa3bf295145196f258 Mon Sep 17 00:00:00 2001
From: Brad Dragun <35275808+LuuBluum@users.noreply.github.com>
Date: Thu, 2 Nov 2023 05:28:16 -0700
Subject: [PATCH] Rational order (#1071)

* Adjust Rationals to use Int instead of QuoInt

* Define ordering over rationals and basic properties

* More properties of rational order

* Clean up definition of order; define trichotomy

* Add multiplication cancelling to rationals

* Fix whitespace

* Remove unnecessary 0<1 proof

* Redefine rec2 with pattern matching
---
 Cubical/Algebra/CommRing/Instances/Int.agda   |   2 +-
 .../Algebra/CommRing/Instances/Rationals.agda |   2 +-
 .../Algebra/Field/Instances/Rationals.agda    |   2 +-
 Cubical/Algebra/Group/ZAction.agda            |   6 +-
 Cubical/Data/Int/Order.agda                   | 258 +++++-
 Cubical/Data/Int/Properties.agda              | 853 +++++++++++++++++-
 Cubical/Data/Rationals/Base.agda              |  23 +-
 .../Data/Rationals/MoreRationals/QuoQ.agda    |   6 +
 .../Rationals/MoreRationals/QuoQ/Base.agda    |  75 ++
 .../MoreRationals/QuoQ/Properties.agda        | 248 +++++
 .../MoreRationals/SigmaQ/Properties.agda      |   2 +-
 Cubical/Data/Rationals/Order.agda             | 623 +++++++++++++
 Cubical/Data/Rationals/Properties.agda        | 424 +++++++--
 Cubical/HITs/SetQuotients/Properties.agda     |  34 +-
 Cubical/Relation/Binary/Base.agda             |   3 +
 .../Tactics/CommRingSolver/RawAlgebra.agda    |   3 +
 16 files changed, 2397 insertions(+), 167 deletions(-)
 create mode 100644 Cubical/Data/Rationals/MoreRationals/QuoQ.agda
 create mode 100644 Cubical/Data/Rationals/MoreRationals/QuoQ/Base.agda
 create mode 100644 Cubical/Data/Rationals/MoreRationals/QuoQ/Properties.agda
 create mode 100644 Cubical/Data/Rationals/Order.agda

diff --git a/Cubical/Algebra/CommRing/Instances/Int.agda b/Cubical/Algebra/CommRing/Instances/Int.agda
index c20c263cb1..2e6a6b5360 100644
--- a/Cubical/Algebra/CommRing/Instances/Int.agda
+++ b/Cubical/Algebra/CommRing/Instances/Int.agda
@@ -22,4 +22,4 @@ isCommRing (snd ℤCommRing) = isCommRingℤ
     isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_
     isCommRingℤ = makeIsCommRing isSetℤ Int.+Assoc (λ _ → refl)
                                  -Cancel Int.+Comm Int.·Assoc
-                                 Int.·Rid ·DistR+ Int.·Comm
+                                 Int.·IdR ·DistR+ Int.·Comm
diff --git a/Cubical/Algebra/CommRing/Instances/Rationals.agda b/Cubical/Algebra/CommRing/Instances/Rationals.agda
index 131125ed07..8b70bf4ec2 100644
--- a/Cubical/Algebra/CommRing/Instances/Rationals.agda
+++ b/Cubical/Algebra/CommRing/Instances/Rationals.agda
@@ -9,7 +9,7 @@ module Cubical.Algebra.CommRing.Instances.Rationals where
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   renaming (ℚ to ℚType ; _+_ to _+ℚ_; _·_ to _·ℚ_; -_ to -ℚ_)
 
 open CommRingStr
diff --git a/Cubical/Algebra/Field/Instances/Rationals.agda b/Cubical/Algebra/Field/Instances/Rationals.agda
index 1c792f45dc..0e1646e889 100644
--- a/Cubical/Algebra/Field/Instances/Rationals.agda
+++ b/Cubical/Algebra/Field/Instances/Rationals.agda
@@ -19,7 +19,7 @@ open import Cubical.Data.Int.MoreInts.QuoInt
            ; ·-zeroˡ to ·ℤ-zeroˡ
            ; ·-identityʳ to ·ℤ-identityʳ)
 open import Cubical.HITs.SetQuotients as SetQuot
-open import Cubical.Data.Rationals
+open import Cubical.Data.Rationals.MoreRationals.QuoQ
   using    (ℚ ; ℕ₊₁→ℤ ; isEquivRel∼)
 
 open import Cubical.Algebra.Field
diff --git a/Cubical/Algebra/Group/ZAction.agda b/Cubical/Algebra/Group/ZAction.agda
index 217a7240f2..38afec7235 100644
--- a/Cubical/Algebra/Group/ZAction.agda
+++ b/Cubical/Algebra/Group/ZAction.agda
@@ -12,9 +12,9 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Powerset
 
 open import Cubical.Data.Sigma
-open import Cubical.Data.Int
+open import Cubical.Data.Int as ℤ
   renaming
-    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc)
+    (_·_ to _*_ ; _+_ to _+ℤ_ ; _-_ to _-ℤ_ ; pos·pos to pos·) hiding (·Assoc; ·IdL; ·IdR)
 open import Cubical.Data.Nat renaming (_·_ to _·ℕ_ ; _+_ to _+ℕ_)
 open import Cubical.Data.Nat.Mod
 open import Cubical.Data.Nat.Order
@@ -410,7 +410,7 @@ characℤ≅ℤ e =
     (λ p → inr (Σ≡Prop (λ _ → isPropIsGroupHom _ _)
                   (Σ≡Prop (λ _ → isPropIsEquiv _)
                     (funExt λ x →
-                      cong (fst (fst e)) (sym (·Rid x))
+                      cong (fst (fst e)) (sym (ℤ.·IdR x))
                       ∙ GroupHomℤ→ℤPres· ((fst (fst e)) , (snd e)) x 1
                       ∙ cong (x *_) p
                       ∙ ·Comm x -1 ))))
diff --git a/Cubical/Data/Int/Order.agda b/Cubical/Data/Int/Order.agda
index 84bb2fb1f5..fac79698da 100644
--- a/Cubical/Data/Int/Order.agda
+++ b/Cubical/Data/Int/Order.agda
@@ -2,12 +2,14 @@
 module Cubical.Data.Int.Order where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Function
 
-open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Empty as ⊥ using (⊥)
 open import Cubical.Data.Int.Base as ℤ
 open import Cubical.Data.Int.Properties as ℤ
 open import Cubical.Data.Nat as ℕ
+open import Cubical.Data.NatPlusOne.Base as ℕ₊₁
 open import Cubical.Data.Sigma
 
 open import Cubical.Relation.Nullary
@@ -47,9 +49,35 @@ isProp≤ {m} {n} (k , p) (l , q)
     lemma : k ≡ l
     lemma = injPos (inj-z+ (p ∙ sym q))
 
+isProp< : isProp (m < n)
+isProp< = isProp≤
+
 zero-≤pos : 0 ≤ pos l
 zero-≤pos {l} = l , (sym (pos0+ (pos l)))
 
+¬-pos<-zero : ¬ (pos k) < 0
+¬-pos<-zero {k} (i , p) = snotz (injPos (pos+ (suc k) i ∙ p))
+
+negsuc<-zero : negsuc k < 0
+negsuc<-zero {k} = k ,
+  ((sucℤ (negsuc k) +pos k)    ≡⟨ sym (sucℤ+ (negsuc k) (pos k)) ⟩
+   sucℤ (negsuc k +pos k)      ≡⟨ +sucℤ (negsuc k) (pos k) ⟩
+   neg (suc k) ℤ.+ pos (suc k) ≡⟨ -Cancel' (pos (suc k)) ⟩
+   pos zero                    ∎)
+
+¬pos≤negsuc : ¬ (pos k) ≤ negsuc l
+¬pos≤negsuc {k} {l} (i , p) = posNotnegsuc (k ℕ.+ i) l (pos+ k i ∙ p)
+
+negsuc<pos : negsuc k < pos l
+negsuc<pos {zero} {zero}   = 0 , refl
+negsuc<pos {zero} {suc l}  = suc l , sym (pos0+ (pos (suc l)))
+negsuc<pos {suc k} {zero}  = suc k , -Cancel' (pos (suc k))
+negsuc<pos {suc k} {suc l} = suc k ℕ.+ suc l
+                           , cong (negsuc k ℤ.+_) (pos+ (suc k) (suc l)) ∙
+                             +Assoc (negsuc k) (pos (suc k)) (pos (suc l)) ∙
+                             cong (ℤ._+ pos (suc l)) (-Cancel' (pos (suc k))) ∙
+                             sym (pos0+ (pos (suc l)))
+
 suc-≤-suc : m ≤ n → sucℤ m ≤ sucℤ n
 suc-≤-suc {m} {n} (k , p) = k , (sym (sucℤ+pos k m) ∙ cong sucℤ p)
 
@@ -91,13 +119,11 @@ pos-≤-pos {k} {l} (i , p) = i ,
          n ℤ.+ o             ∎)
 
 ≤SumRightPos : n ≤ pos k ℤ.+ n
-≤SumRightPos {n} {k} = subst (_≤ pos k ℤ.+ n) (sym (pos0+ n)) (≤-+o {o = n} (zero-≤pos {k}))
+≤SumRightPos {n} {k}
+  = subst (_≤ pos k ℤ.+ n) (sym (pos0+ n)) (≤-+o {o = n} (zero-≤pos {k}))
 
 ≤-o+ : m ≤ n → o ℤ.+ m ≤ o ℤ.+ n
-≤-o+ {m} {n} {o}
-  = subst (_≤ o ℤ.+ n) (+Comm m o)
-  ∘ subst (m ℤ.+ o ≤_) (+Comm n o)
-  ∘ ≤-+o {o = o}
+≤-o+ {m} {n} {o} = subst2 (_≤_) (+Comm m o) (+Comm n o) ∘ ≤-+o {o = o}
 
 ≤SumLeftPos : n ≤ n ℤ.+ pos k
 ≤SumLeftPos {n} {k} = ≤-o+ {o = n} (zero-≤pos {k})
@@ -175,18 +201,35 @@ isAntisym≤ {m} {n} (i , p) (j , q)
    (m +pos i) ℤ.· pos k             ≡⟨ cong (ℤ._· pos k) p ⟩
    n ℤ.· pos k                      ∎)
 
+0≤o→≤-·o : 0 ≤ o → m ≤ n → m ℤ.· o ≤ n ℤ.· o
+0≤o→≤-·o {pos o} 0≤o m≤n = ≤-·o {k = o} m≤n
+0≤o→≤-·o {negsuc o} 0≤o _ = ⊥.rec (¬pos≤negsuc 0≤o)
+
+<-·o : m < n → m ℤ.· (pos (suc k)) < n ℤ.· (pos (suc k))
+<-·o {m} {n} {k} (i , p) = (i ℕ.· suc k ℕ.+ k) ,
+    ((sucℤ (m ℤ.· pos (suc k)) +pos (i ℕ.· suc k ℕ.+ k))        ≡⟨ cong (sucℤ (m ℤ.· pos (suc k)) ℤ.+_)
+                                                                       (pos+ (i ℕ.· suc k) k) ⟩
+      sucℤ (m ℤ.· pos (suc k)) ℤ.+ (pos (i ℕ.· suc k) +pos k)   ≡⟨ cong (sucℤ (m ℤ.· pos (suc k)) ℤ.+_)
+                                                                       (+Comm (pos (i ℕ.· suc k)) (pos k)) ⟩
+      sucℤ (m ℤ.· pos (suc k)) ℤ.+ (pos k +pos (i ℕ.· suc k))   ≡⟨ +Assoc (sucℤ (m ℤ.· pos (suc k))) (pos k) (pos (i ℕ.· suc k)) ⟩
+    ((sucℤ (m ℤ.· pos (suc k)) +pos k) +pos (i ℕ.· suc k))      ≡⟨ cong (_+pos (i ℕ.· suc k))
+                                                                       (sym (sucℤ+pos k (m ℤ.· pos (suc k)))) ⟩
+     (sucℤ ((m ℤ.· pos (suc k)) +pos k) +pos (i ℕ.· suc k))     ≡⟨ cong (_+pos (i ℕ.· suc k)) (+sucℤ (m ℤ.· pos (suc k)) (pos k)) ⟩
+   (((m ℤ.· pos (suc k)) ℤ.+ (pos (suc k))) +pos (i ℕ.· suc k)) ≡⟨ cong (_+pos (i ℕ.· suc k))
+                                                                       (+Comm (m ℤ.· pos (suc k)) (pos (suc k))) ⟩
+     ((pos (suc k) ℤ.+ m ℤ.· pos (suc k)) +pos (i ℕ.· suc k))    ≡⟨ cong (_+pos (i ℕ.· suc k)) (sym (sucℤ· m (pos (suc k)))) ⟩
+    (((sucℤ m) ℤ.· pos (suc k)) +pos (i ℕ.· suc k))              ≡⟨ cong ((sucℤ m) ℤ.· pos (suc k) ℤ.+_)
+                                                                       (pos·pos i (suc k)) ⟩
+     ((sucℤ m) ℤ.· pos (suc k)) ℤ.+ pos i ℤ.· pos (suc k)        ≡⟨ sym (·DistL+ ((sucℤ m)) (pos i) (pos (suc k))) ⟩
+     ((sucℤ m) +pos i) ℤ.· pos (suc k)                            ≡⟨ cong (ℤ._· pos (suc k)) p ⟩
+      n ℤ.· pos (suc k)                                              ∎)
+
+
 <-o+-cancel : o ℤ.+ m < o ℤ.+ n → m < n
 <-o+-cancel {o} {m} {n} = ≤-o+-cancel ∘ subst (_≤ o ℤ.+ n) (+sucℤ o m)
 
-¬-pos<-zero : ¬ (pos k) < 0
-¬-pos<-zero {k} (i , p) = snotz (injPos (pos+ (suc k) i ∙ p))
-
-negsuc<-zero : negsuc k < 0
-negsuc<-zero {k} = k ,
-  ((sucℤ (negsuc k) +pos k)    ≡⟨ sym (sucℤ+ (negsuc k) (pos k)) ⟩
-   sucℤ (negsuc k +pos k)      ≡⟨ +sucℤ (negsuc k) (pos k) ⟩
-   neg (suc k) ℤ.+ pos (suc k) ≡⟨ -Cancel' (pos (suc k)) ⟩
-   pos zero                    ∎)
+<-weaken : m < n → m ≤ n
+<-weaken {m} (i , p) = (suc i) , sucℤ+ m (pos i) ∙ p
 
 isIrrefl< : ¬ m < m
 isIrrefl< {pos zero} (i , p) = snotz (injPos (pos+ (suc zero) i ∙ p))
@@ -203,6 +246,11 @@ isIrrefl< {negsuc (suc n)} (i , p) = isIrrefl< {m = negsuc n} (i ,
    sucℤ (negsuc n +pos i)   ≡⟨ cong sucℤ p ⟩
    negsuc n                 ∎))
 
+0<o→<-·o : 0 < o → m < n → m ℤ.· o < n ℤ.· o
+0<o→<-·o {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
+0<o→<-·o {pos (suc o)} 0<o m<n = <-·o {k = o} m<n
+0<o→<-·o {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc (<-weaken 0<o))
+
 pos≤0→≡0 : pos k ≤ 0 → pos k ≡ 0
 pos≤0→≡0 {zero} _ = refl
 pos≤0→≡0 {suc k} p = ⊥.rec (¬-pos<-zero {k = k} p)
@@ -216,9 +264,6 @@ predℤ-≤-predℤ {m} {n} (i , p) = i ,
 ¬m+posk<m : ¬ m ℤ.+ pos k < m
 ¬m+posk<m {m} {k} = ¬-pos<-zero ∘ <-o+-cancel {o = m} {m = pos k} {n = 0}
 
-<-weaken : m < n → m ≤ n
-<-weaken {m} (i , p) = (suc i) , sucℤ+ m (pos i) ∙ p
-
 ≤<-trans : o ≤ m → m < n → o < n
 ≤<-trans p = isTrans≤ (suc-≤-suc p)
 
@@ -252,34 +297,159 @@ isAsym< m<n = isIrrefl< ∘ <≤-trans m<n
 -pos≤ : m - (pos k) ≤ m
 -pos≤ {m} {k} = k , minusPlus (pos k) m
 
-≤-max : m ≤ ℤ.max m n
-≤-max {pos zero} {pos m} = zero-≤pos
-≤-max {pos (suc m)} {pos zero} = isRefl≤
-≤-max {pos (suc m)} {pos (suc n)} = suc-≤-suc (≤-max {m = pos m} {n = pos n})
-≤-max {pos zero} {negsuc n} = isRefl≤
-≤-max {pos (suc m)} {negsuc n} = isRefl≤
-≤-max {negsuc m} {pos zero} = negsuc<-zero
-≤-max {negsuc m} {pos (suc n)} = isTrans≤ negsuc<-zero zero-≤pos
-≤-max {negsuc zero} {negsuc n} = isRefl≤
-≤-max {negsuc (suc m)} {negsuc zero} = negsuc-≤-negsuc zero-≤pos
-≤-max {negsuc (suc m)} {negsuc (suc n)} = pred-≤-pred (subst (negsuc m ≤_)
+·suc≤0 : m ℤ.· (pos (suc k)) ≤ 0 → m ≤ 0
+·suc≤0 {pos n} {k} (i , p) = 0 ,
+  cong pos (sym (0≡n·sm→0≡n
+           (sym (m+n≡0→m≡0×n≡0
+                (injPos (pos+ (n ℕ.· suc k) i ∙
+                         cong (_+pos i) (pos·pos n (suc k)) ∙
+                         p)) .fst))))
+·suc≤0 {negsuc _} _ = negsuc<-zero
+
+·suc<0 : m ℤ.· (pos (suc k)) < 0 → m < 0
+·suc<0 {pos n} {k} (i , p) =
+  ⊥.rec (snotz (injPos
+               (pos+ (suc (n ℕ.· suc k)) i ∙
+                cong (λ x → sucℤ x +pos i) (pos·pos n (suc k)) ∙
+                p)))
+·suc<0 {negsuc _} _ = negsuc<-zero
+
+≤-·o-cancel : m ℤ.· (pos (suc k)) ≤ n ℤ.· (pos (suc k)) → m ≤ n
+≤-·o-cancel {m} {k} {n} mk≤nk =
+  subst2 _≤_
+         (minusPlus n m)
+         (+Comm 0 n)
+         (≤-+o {o = n}
+               (·suc≤0 (subst2 _≤_
+                               (cong (m ℤ.· pos (suc k) ℤ.+_) (-DistL· n (pos (suc k))) ∙
+                                 sym (·DistL+ m (- n) (pos (suc k))))
+                               (-Cancel (n ℤ.· pos (suc k)))
+                               (≤-+o {o = - (n ℤ.· pos (suc k))} mk≤nk))))
+
+0<o→≤-·o-cancel : 0 < o → m ℤ.· o ≤ n ℤ.· o → m ≤ n
+0<o→≤-·o-cancel {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
+0<o→≤-·o-cancel {pos (suc o)} 0<o mo≤no = ≤-·o-cancel {k = o} mo≤no
+0<o→≤-·o-cancel {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc 0<o)
+
+≤-o·-cancel : (pos (suc k)) ℤ.· m ≤ (pos (suc k)) ℤ.· n → m ≤ n
+≤-o·-cancel {k} {m} {n} = ≤-·o-cancel ∘ (subst2 _≤_ (·Comm (pos (suc k)) m) (·Comm (pos (suc k)) n))
+
+<-·o-cancel : m ℤ.· (pos (suc k)) < n ℤ.· (pos (suc k)) → m < n
+<-·o-cancel {m} {k} {n} mk<nk =
+  subst2 _<_
+         (minusPlus n m)
+         (+Comm 0 n)
+         (<-+o {o = n}
+               (·suc<0 (subst2 _<_
+                               (cong (m ℤ.· pos (suc k) ℤ.+_) (-DistL· n (pos (suc k))) ∙
+                                 sym (·DistL+ m (- n) (pos (suc k))))
+                               (-Cancel (n ℤ.· pos (suc k)))
+                               (<-+o {o = - (n ℤ.· pos (suc k))} mk<nk))))
+
+0<o→<-·o-cancel : 0 < o → m ℤ.· o < n ℤ.· o → m < n
+0<o→<-·o-cancel {pos zero} 0<o _ = ⊥.rec (isIrrefl< 0<o)
+0<o→<-·o-cancel {pos (suc o)} 0<o mo<no = <-·o-cancel {k = o} mo<no
+0<o→<-·o-cancel {negsuc o} 0<o _ = ⊥.rec (¬pos≤negsuc 0<o)
+
+<-o·-cancel : (pos (suc k)) ℤ.· m < (pos (suc k)) ℤ.· n → m < n
+<-o·-cancel {k} {m} {n} = <-·o-cancel ∘ (subst2 _<_ (·Comm (pos (suc k)) m) (·Comm (pos (suc k)) n))
+
+-Dist≤ : m ≤ n → (- n) ≤ (- m)
+-Dist≤ {pos zero} {pos zero} _ = isRefl≤
+-Dist≤ {pos zero} {pos (suc n)} _ = <-weaken negsuc<-zero
+-Dist≤ {pos (suc m)} {pos zero} = ⊥.rec ∘ snotz ∘ injPos ∘ pos≤0→≡0
+-Dist≤ {pos (suc m)} {pos (suc n)} = suc-≤-suc ∘ negsuc-≤-negsuc
+-Dist≤ {pos m} {negsuc n} = ⊥.rec ∘ ¬pos≤negsuc
+-Dist≤ {negsuc zero} {pos zero} = suc-≤-suc
+-Dist≤ {negsuc zero} {pos (suc n)} = suc-≤-suc ∘ -Dist≤ ∘ suc-≤-suc
+-Dist≤ {negsuc (suc m)} {pos zero} _ = zero-≤pos
+-Dist≤ {negsuc (suc m)} {pos (suc n)} _ = negsuc<pos
+-Dist≤ {negsuc m} {negsuc n} = suc-≤-suc ∘ pos-≤-pos
+
+-Dist< : m < n → (- n) < (- m)
+-Dist< {m} {n} = subst (- n <_) (cong sucℤ (-sucℤ m) ∙ sucPred (- m))
+               ∘ suc-≤-suc
+               ∘ -Dist≤
+
+≤max : m ≤ ℤ.max m n
+≤max {pos zero} {pos m} = zero-≤pos
+≤max {pos (suc m)} {pos zero} = isRefl≤
+≤max {pos (suc m)} {pos (suc n)} = suc-≤-suc (≤max {m = pos m} {n = pos n})
+≤max {pos zero} {negsuc n} = isRefl≤
+≤max {pos (suc m)} {negsuc n} = isRefl≤
+≤max {negsuc m} {pos zero} = negsuc<-zero
+≤max {negsuc m} {pos (suc n)} = isTrans≤ negsuc<-zero zero-≤pos
+≤max {negsuc zero} {negsuc n} = isRefl≤
+≤max {negsuc (suc m)} {negsuc zero} = negsuc-≤-negsuc zero-≤pos
+≤max {negsuc (suc m)} {negsuc (suc n)} = pred-≤-pred (subst (negsuc m ≤_)
                                         (sym (sucPred (ℤ.max (negsuc m) (negsuc n))))
-                                        (≤-max {m = negsuc m} {n = negsuc n}))
-
-min-≤ : ℤ.min m n ≤ m
-min-≤ {pos zero} {pos n} = isRefl≤
-min-≤ {pos (suc m)} {pos zero} = zero-≤pos
-min-≤ {pos (suc m)} {pos (suc n)} = suc-≤-suc (min-≤ {m = pos m} {n = pos n})
-min-≤ {pos zero} {negsuc n} = negsuc<-zero
-min-≤ {pos (suc m)} {negsuc n} = isTrans≤ negsuc<-zero zero-≤pos
-min-≤ {negsuc zero} {pos n} = isRefl≤
-min-≤ {negsuc (suc m)} {pos n} = isRefl≤
-min-≤ {negsuc zero} {negsuc zero} = isRefl≤
-min-≤ {negsuc zero} {negsuc (suc n)} = negsuc-≤-negsuc zero-≤pos
-min-≤ {negsuc (suc m)} {negsuc zero} = isRefl≤
-min-≤ {negsuc (suc m)} {negsuc (suc n)} = pred-≤-pred (subst (_≤ negsuc m)
+                                        (≤max {m = negsuc m} {n = negsuc n}))
+
+≤→max : m ≤ n → ℤ.max m n ≡ n
+≤→max {pos zero} {pos n} m≤n = refl
+≤→max {pos (suc m)} {pos zero} m≤n = ⊥.rec (snotz (injPos (pos≤0→≡0 m≤n)))
+≤→max {pos (suc m)} {pos (suc n)} m≤n
+  = cong sucℤ (≤→max {m = pos m} {n = pos n} (pred-≤-pred m≤n))
+≤→max {pos m} {negsuc n} m≤n = ⊥.rec (¬pos≤negsuc m≤n)
+≤→max {negsuc m} {pos n} m≤n = refl
+≤→max {negsuc zero} {negsuc zero} m≤n = refl
+≤→max {negsuc zero} {negsuc (suc n)} m≤n
+  = ⊥.rec (snotz (injPos (pos≤0→≡0 (pos-≤-pos m≤n))))
+≤→max {negsuc (suc m)} {negsuc zero} m≤n = refl
+≤→max {negsuc (suc m)} {negsuc (suc n)} m≤n
+  = cong predℤ (≤→max {m = negsuc m} {n = negsuc n} (suc-≤-suc m≤n))
+
+min≤ : ℤ.min m n ≤ m
+min≤ {pos zero} {pos n} = isRefl≤
+min≤ {pos (suc m)} {pos zero} = zero-≤pos
+min≤ {pos (suc m)} {pos (suc n)} = suc-≤-suc (min≤ {m = pos m} {n = pos n})
+min≤ {pos zero} {negsuc n} = negsuc<-zero
+min≤ {pos (suc m)} {negsuc n} = isTrans≤ negsuc<-zero zero-≤pos
+min≤ {negsuc zero} {pos n} = isRefl≤
+min≤ {negsuc (suc m)} {pos n} = isRefl≤
+min≤ {negsuc zero} {negsuc zero} = isRefl≤
+min≤ {negsuc zero} {negsuc (suc n)} = negsuc-≤-negsuc zero-≤pos
+min≤ {negsuc (suc m)} {negsuc zero} = isRefl≤
+min≤ {negsuc (suc m)} {negsuc (suc n)} = pred-≤-pred (subst (_≤ negsuc m)
                                         (sym (sucPred (ℤ.min (negsuc m) (negsuc n))))
-                                        (min-≤ {m = negsuc m} {n = negsuc n}))
+                                        (min≤ {m = negsuc m} {n = negsuc n}))
+
+≤→min : m ≤ n → ℤ.min m n ≡ m
+≤→min {pos zero} {pos n} _ = refl
+≤→min {pos (suc m)} {pos zero} m≤n = ⊥.rec (snotz (injPos (pos≤0→≡0 m≤n)))
+≤→min {pos (suc m)} {pos (suc n)} m≤n
+  = cong sucℤ (≤→min {m = pos m} {n = pos n} (pred-≤-pred m≤n))
+≤→min {pos m} {negsuc n} m≤n = ⊥.rec (¬pos≤negsuc m≤n)
+≤→min {negsuc m} {pos n} _ = refl
+≤→min {negsuc zero} {negsuc zero} _ = refl
+≤→min {negsuc zero} {negsuc (suc n)} m≤n
+  = ⊥.rec (snotz (injPos (pos≤0→≡0 (pos-≤-pos m≤n))))
+≤→min {negsuc (suc m)} {negsuc zero} _ = refl
+≤→min {negsuc (suc m)} {negsuc (suc n)} m≤n
+  = cong predℤ (≤→min {m = negsuc m} {n = negsuc n} (suc-≤-suc m≤n))
+
+≤MonotoneMin : m ≤ n → o ≤ s → ℤ.min m o ≤ ℤ.min n s
+≤MonotoneMin {m} {n} {o} {s} m≤n o≤s
+  = subst (_≤ ℤ.min n s)
+          (sym (minAssoc n s (ℤ.min m o)) ∙
+           cong (ℤ.min n) (minAssoc s m o ∙
+                           cong (λ a → ℤ.min a o) (ℤ.minComm s m) ∙
+                                 sym (minAssoc m s o)) ∙
+                           minAssoc n m (ℤ.min s o) ∙
+           cong₂ ℤ.min (ℤ.minComm n m ∙ ≤→min m≤n)
+                       (ℤ.minComm s o ∙ ≤→min o≤s))
+           (min≤ {m = ℤ.min n s} {n = ℤ.min m o})
+
+≤MonotoneMax : m ≤ n → o ≤ s → ℤ.max m o ≤ ℤ.max n s
+≤MonotoneMax {m} {n} {o} {s} m≤n o≤s
+  = subst (ℤ.max m o ≤_)
+          (sym (maxAssoc m o (ℤ.max n s)) ∙
+           cong (ℤ.max m) (maxAssoc o n s ∙
+                           cong (λ a → ℤ.max a s) (ℤ.maxComm o n) ∙
+                                 sym (maxAssoc n o s)) ∙
+                           maxAssoc m n (ℤ.max o s) ∙
+           cong₂ ℤ.max (≤→max m≤n) (≤→max o≤s))
+          (≤max {m = ℤ.max m o} {n = ℤ.max n s})
 
 ≤Dec : ∀ m n → Dec (m ≤ n)
 ≤Dec (pos zero) (pos n) = yes zero-≤pos
diff --git a/Cubical/Data/Int/Properties.agda b/Cubical/Data/Int/Properties.agda
index 37cce05b7d..0d096a8eb4 100644
--- a/Cubical/Data/Int/Properties.agda
+++ b/Cubical/Data/Int/Properties.agda
@@ -48,6 +48,12 @@ minComm (negsuc zero) (negsuc (suc m)) = refl
 minComm (negsuc (suc n)) (negsuc zero) = refl
 minComm (negsuc (suc n)) (negsuc (suc m)) = cong predℤ (minComm (negsuc n) (negsuc m))
 
+minIdem : ∀ n → min n n ≡ n
+minIdem (pos zero) = refl
+minIdem (pos (suc n)) = cong sucℤ (minIdem (pos n))
+minIdem (negsuc zero) = refl
+minIdem (negsuc (suc n)) = cong predℤ (minIdem (negsuc n))
+
 max : ℤ → ℤ → ℤ
 max (pos zero) (pos m) = pos m
 max (pos (suc n)) (pos zero) = pos (suc n)
@@ -76,6 +82,12 @@ maxComm (negsuc zero) (negsuc (suc m)) = refl
 maxComm (negsuc (suc n)) (negsuc zero) = refl
 maxComm (negsuc (suc n)) (negsuc (suc m)) = cong predℤ (maxComm (negsuc n) (negsuc m))
 
+maxIdem : ∀ n → max n n ≡ n
+maxIdem (pos zero) = refl
+maxIdem (pos (suc n)) = cong sucℤ (maxIdem (pos n))
+maxIdem (negsuc zero) = refl
+maxIdem (negsuc (suc n)) = cong predℤ (maxIdem (negsuc n))
+
 sucPred : ∀ i → sucℤ (predℤ i) ≡ i
 sucPred (pos zero)    = refl
 sucPred (pos (suc n)) = refl
@@ -86,6 +98,288 @@ predSuc (pos n)          = refl
 predSuc (negsuc zero)    = refl
 predSuc (negsuc (suc n)) = refl
 
+sucDistMin : ∀ m n → sucℤ (min m n) ≡ min (sucℤ m) (sucℤ n)
+sucDistMin (pos zero) (pos zero) = refl
+sucDistMin (pos zero) (pos (suc n)) = refl
+sucDistMin (pos (suc m)) (pos zero) = refl
+sucDistMin (pos (suc m)) (pos (suc n)) = refl
+sucDistMin (pos zero) (negsuc zero) = refl
+sucDistMin (pos zero) (negsuc (suc n)) = refl
+sucDistMin (pos (suc m)) (negsuc zero) = refl
+sucDistMin (pos (suc m)) (negsuc (suc n)) = refl
+sucDistMin (negsuc zero) (pos zero) = refl
+sucDistMin (negsuc zero) (pos (suc n)) = refl
+sucDistMin (negsuc (suc m)) (pos zero) = refl
+sucDistMin (negsuc (suc m)) (pos (suc 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)) = sucPred _
+
+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) = minComm (negsuc zero) (pos m)
+predDistMin (pos (suc m)) (pos (suc n)) = predSuc _
+predDistMin (pos zero) (negsuc zero) = refl
+predDistMin (pos zero) (negsuc (suc n)) = refl
+predDistMin (pos (suc m)) (negsuc zero) = minComm (negsuc 1) (pos m)
+predDistMin (pos (suc m)) (negsuc (suc n)) = minComm (negsuc (suc (suc n))) (pos m)
+predDistMin (negsuc zero) (pos zero) = refl
+predDistMin (negsuc zero) (pos (suc n)) = refl
+predDistMin (negsuc (suc m)) (pos zero) = refl
+predDistMin (negsuc (suc m)) (pos (suc n)) = refl
+predDistMin (negsuc zero) (negsuc zero) = refl
+predDistMin (negsuc zero) (negsuc (suc n)) = refl
+predDistMin (negsuc (suc m)) (negsuc zero) = refl
+predDistMin (negsuc (suc m)) (negsuc (suc n)) = refl
+
+minSucL : ∀ m → min (sucℤ m) m ≡ m
+minSucL (pos zero) = refl
+minSucL (pos (suc m)) = cong sucℤ (minSucL (pos m))
+minSucL (negsuc zero) = refl
+minSucL (negsuc (suc m))
+  = sym (cong predℤ (sym (minSucL (negsuc m))) ∙
+         predDistMin (sucℤ (negsuc m)) (negsuc m) ∙
+         cong (λ a → min a (negsuc (suc m))) (predSuc (negsuc m)))
+
+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)) = minSucR (pos m)
+minPredL (negsuc zero) = refl
+minPredL (negsuc (suc m)) = cong predℤ (minPredL (negsuc m))
+
+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 zero) (pos zero) = refl
+sucDistMax (pos zero) (pos (suc n)) = refl
+sucDistMax (pos (suc m)) (pos zero) = refl
+sucDistMax (pos (suc m)) (pos (suc n)) = refl
+sucDistMax (pos zero) (negsuc zero) = refl
+sucDistMax (pos zero) (negsuc (suc n)) = refl
+sucDistMax (pos (suc m)) (negsuc zero) = refl
+sucDistMax (pos (suc m)) (negsuc (suc n)) = refl
+sucDistMax (negsuc zero) (pos zero) = refl
+sucDistMax (negsuc zero) (pos (suc n)) = refl
+sucDistMax (negsuc (suc m)) (pos zero) = refl
+sucDistMax (negsuc (suc m)) (pos (suc 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)) = sucPred _
+
+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) = maxComm (negsuc zero) (pos m)
+predDistMax (pos (suc m)) (pos (suc n)) = predSuc _
+predDistMax (pos zero) (negsuc zero) = refl
+predDistMax (pos zero) (negsuc (suc n)) = refl
+predDistMax (pos (suc m)) (negsuc zero) = maxComm (negsuc 1) (pos m)
+predDistMax (pos (suc m)) (negsuc (suc n)) = maxComm (negsuc (suc (suc n))) (pos m)
+predDistMax (negsuc zero) (pos zero) = refl
+predDistMax (negsuc zero) (pos (suc n)) = refl
+predDistMax (negsuc (suc m)) (pos zero) = refl
+predDistMax (negsuc (suc m)) (pos (suc n)) = refl
+predDistMax (negsuc zero) (negsuc zero) = refl
+predDistMax (negsuc zero) (negsuc (suc n)) = refl
+predDistMax (negsuc (suc m)) (negsuc zero) = refl
+predDistMax (negsuc (suc m)) (negsuc (suc n)) = refl
+
+maxSucL : ∀ m → max (sucℤ m) m ≡ sucℤ m
+maxSucL (pos zero) = refl
+maxSucL (pos (suc m)) = cong sucℤ (maxSucL (pos m))
+maxSucL (negsuc zero) = refl
+maxSucL (negsuc (suc m))
+  = cong (λ a → max a (negsuc (suc m))) (sym (predSuc (negsuc m))) ∙
+    sym (predDistMax (sucℤ (negsuc m)) (negsuc m)) ∙
+    cong predℤ (maxSucL (negsuc m)) ∙
+    predSuc (negsuc m)
+
+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)) = maxSucR (pos m)
+maxPredL (negsuc zero) = refl
+maxPredL (negsuc (suc m)) = cong predℤ (maxPredL (negsuc m))
+
+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 zero) (pos zero) (pos z) = refl
+minAssoc (pos zero) (pos (suc y)) (pos zero) = refl
+minAssoc (pos zero) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMin (negsuc zero) (min (pos y) (pos z))) ∙
+    cong sucℤ (minAssoc (negsuc zero) (pos y) (pos z))
+minAssoc (pos (suc x)) (pos zero) (pos z) = refl
+minAssoc (pos (suc x)) (pos (suc y)) (pos zero)
+  = cong (min (pos (suc x))) (sym (sucDistMin (pos y) (negsuc zero))) ∙
+    sym (sucDistMin (pos x) (min (pos y) (negsuc zero))) ∙
+    cong sucℤ (minAssoc (pos x) (pos y) (negsuc zero)) ∙
+    sucDistMin (min (pos x) (pos y)) (negsuc zero)
+minAssoc (pos (suc x)) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMin (pos x) (min (pos y) (pos z))) ∙
+    cong sucℤ (minAssoc (pos x) (pos y) (pos z)) ∙
+    sucDistMin (min (pos x) (pos y)) (pos z)
+minAssoc (pos zero) (pos zero) (negsuc z) = refl
+minAssoc (pos zero) (pos (suc y)) (negsuc z) = refl
+minAssoc (pos (suc x)) (pos zero) (negsuc z) = refl
+minAssoc (pos (suc x)) (pos (suc y)) (negsuc z)
+  = cong (min (pos (suc x))) (sym (sucDistMin (pos y) (negsuc (suc z)))) ∙
+    sym (sucDistMin (pos x) (min (pos y) (negsuc (suc z)))) ∙
+    cong sucℤ (minAssoc (pos x) (pos y) (negsuc (suc z))) ∙
+    sucDistMin (min (pos x) (pos y)) (negsuc (suc z))
+minAssoc (pos zero) (negsuc y) (pos z) = refl
+minAssoc (pos (suc x)) (negsuc y) (pos z) = refl
+minAssoc (pos zero) (negsuc zero) (negsuc z) = refl
+minAssoc (pos zero) (negsuc (suc y)) (negsuc zero) = refl
+minAssoc (pos zero) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMin (pos 1) (min (negsuc y) (negsuc z))) ∙
+    cong predℤ (minAssoc (pos 1) (negsuc y) (negsuc z)) ∙
+    predDistMin (min (pos 1) (negsuc y)) (negsuc z)
+minAssoc (pos (suc x)) (negsuc zero) (negsuc z) = refl
+minAssoc (pos (suc x)) (negsuc (suc y)) (negsuc zero) = refl
+minAssoc (pos (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMin (pos (suc (suc x))) (min (negsuc y) (negsuc z))) ∙
+    cong predℤ (minAssoc (pos (suc (suc x))) (negsuc y) (negsuc z)) ∙
+    predDistMin (min (pos (suc (suc x))) (negsuc y)) (negsuc z)
+minAssoc (negsuc x) (pos zero) (pos z) = refl
+minAssoc (negsuc x) (pos (suc y)) (pos zero) = refl
+minAssoc (negsuc zero) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMin (negsuc 1) (min (pos y) (pos z))) ∙
+    cong sucℤ (minAssoc (negsuc 1) (pos y) (pos z)) ∙
+    sucDistMin (min (negsuc 1) (pos y)) (pos z)
+minAssoc (negsuc (suc x)) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMin (negsuc (suc (suc x))) (min (pos y) (pos z))) ∙
+    cong sucℤ (minAssoc (negsuc (suc (suc x))) (pos y) (pos z))
+minAssoc (negsuc x) (pos zero) (negsuc z) = refl
+minAssoc (negsuc x) (pos (suc y)) (negsuc z) = refl
+minAssoc (negsuc zero) (negsuc y) (pos z) = refl
+minAssoc (negsuc (suc x)) (negsuc zero) (pos z) = refl
+minAssoc (negsuc (suc x)) (negsuc (suc y)) (pos z)
+  = cong predℤ (minAssoc (negsuc x) (negsuc y) (pos (suc z))) ∙
+    predDistMin (min (negsuc x) (negsuc y)) (pos (suc z))
+minAssoc (negsuc zero) (negsuc zero) (negsuc z) = refl
+minAssoc (negsuc zero) (negsuc (suc y)) (negsuc zero) = refl
+minAssoc (negsuc zero) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMin (pos zero) (min (negsuc y) (negsuc z))) ∙
+    cong predℤ (minAssoc (pos zero) (negsuc y) (negsuc z))
+minAssoc (negsuc (suc x)) (negsuc zero) (negsuc z) = refl
+minAssoc (negsuc (suc x)) (negsuc (suc y)) (negsuc zero)
+  = cong predℤ (minAssoc (negsuc x) (negsuc y) (pos zero)) ∙
+    predDistMin (min (negsuc x) (negsuc y)) (pos zero)
+minAssoc (negsuc (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMin (negsuc x) (min (negsuc y) (negsuc z))) ∙
+    cong predℤ (minAssoc (negsuc x) (negsuc y) (negsuc z)) ∙
+    predDistMin (min (negsuc x) (negsuc y)) (negsuc z)
+
+maxAssoc : ∀ x y z → max x (max y z) ≡ max (max x y) z
+maxAssoc (pos zero) (pos zero) (pos z) = refl
+maxAssoc (pos zero) (pos (suc y)) (pos zero) = refl
+maxAssoc (pos zero) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMax (negsuc zero) (max (pos y) (pos z))) ∙
+    cong sucℤ (maxAssoc (negsuc zero) (pos y) (pos z))
+maxAssoc (pos (suc x)) (pos zero) (pos z) = refl
+maxAssoc (pos (suc x)) (pos (suc y)) (pos zero)
+  = cong (max (pos (suc x))) (sym (sucDistMax (pos y) (negsuc zero))) ∙
+    sym (sucDistMax (pos x) (max (pos y) (negsuc zero))) ∙
+    cong sucℤ (maxAssoc (pos x) (pos y) (negsuc zero)) ∙
+    sucDistMax (max (pos x) (pos y)) (negsuc zero)
+maxAssoc (pos (suc x)) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMax (pos x) (max (pos y) (pos z))) ∙
+    cong sucℤ (maxAssoc (pos x) (pos y) (pos z)) ∙
+    sucDistMax (max (pos x) (pos y)) (pos z)
+maxAssoc (pos zero) (pos zero) (negsuc z) = refl
+maxAssoc (pos zero) (pos (suc y)) (negsuc z) = refl
+maxAssoc (pos (suc x)) (pos zero) (negsuc z) = refl
+maxAssoc (pos (suc x)) (pos (suc y)) (negsuc z)
+  = cong (max (pos (suc x))) (sym (sucDistMax (pos y) (negsuc (suc z)))) ∙
+    sym (sucDistMax (pos x) (max (pos y) (negsuc (suc z)))) ∙
+    cong sucℤ (maxAssoc (pos x) (pos y) (negsuc (suc z))) ∙
+    sucDistMax (max (pos x) (pos y)) (negsuc (suc z))
+maxAssoc (pos zero) (negsuc y) (pos z) = refl
+maxAssoc (pos (suc x)) (negsuc y) (pos z) = refl
+maxAssoc (pos zero) (negsuc zero) (negsuc z) = refl
+maxAssoc (pos zero) (negsuc (suc y)) (negsuc zero) = refl
+maxAssoc (pos zero) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMax (pos 1) (max (negsuc y) (negsuc z))) ∙
+    cong predℤ (maxAssoc (pos 1) (negsuc y) (negsuc z)) ∙
+    predDistMax (max (pos 1) (negsuc y)) (negsuc z)
+maxAssoc (pos (suc x)) (negsuc zero) (negsuc z) = refl
+maxAssoc (pos (suc x)) (negsuc (suc y)) (negsuc zero) = refl
+maxAssoc (pos (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMax (pos (suc (suc x))) (max (negsuc y) (negsuc z))) ∙
+    cong predℤ (maxAssoc (pos (suc (suc x))) (negsuc y) (negsuc z)) ∙
+    predDistMax (max (pos (suc (suc x))) (negsuc y)) (negsuc z)
+maxAssoc (negsuc x) (pos zero) (pos z) = refl
+maxAssoc (negsuc x) (pos (suc y)) (pos zero) = refl
+maxAssoc (negsuc zero) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMax (negsuc 1) (max (pos y) (pos z))) ∙
+    cong sucℤ (maxAssoc (negsuc 1) (pos y) (pos z)) ∙
+    sucDistMax (max (negsuc 1) (pos y)) (pos z)
+maxAssoc (negsuc (suc x)) (pos (suc y)) (pos (suc z))
+  = sym (sucDistMax (negsuc (suc (suc x))) (max (pos y) (pos z))) ∙
+    cong sucℤ (maxAssoc (negsuc (suc (suc x))) (pos y) (pos z))
+maxAssoc (negsuc x) (pos zero) (negsuc z) = refl
+maxAssoc (negsuc x) (pos (suc y)) (negsuc z) = refl
+maxAssoc (negsuc zero) (negsuc y) (pos z) = refl
+maxAssoc (negsuc (suc x)) (negsuc zero) (pos z) = refl
+maxAssoc (negsuc (suc x)) (negsuc (suc y)) (pos z)
+  = cong predℤ (maxAssoc (negsuc x) (negsuc y) (pos (suc z))) ∙
+    predDistMax (max (negsuc x) (negsuc y)) (pos (suc z))
+maxAssoc (negsuc zero) (negsuc zero) (negsuc z) = refl
+maxAssoc (negsuc zero) (negsuc (suc y)) (negsuc zero) = refl
+maxAssoc (negsuc zero) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMax (pos zero) (max (negsuc y) (negsuc z))) ∙
+    cong predℤ (maxAssoc (pos zero) (negsuc y) (negsuc z))
+maxAssoc (negsuc (suc x)) (negsuc zero) (negsuc z) = refl
+maxAssoc (negsuc (suc x)) (negsuc (suc y)) (negsuc zero)
+  = cong predℤ (maxAssoc (negsuc x) (negsuc y) (pos zero)) ∙
+    predDistMax (max (negsuc x) (negsuc y)) (pos zero)
+maxAssoc (negsuc (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (predDistMax (negsuc x) (max (negsuc y) (negsuc z))) ∙
+    cong predℤ (maxAssoc (negsuc x) (negsuc y) (negsuc z)) ∙
+    predDistMax (max (negsuc x) (negsuc y)) (negsuc z)
+
+minAbsorbLMax : ∀ x y → min x (max x y) ≡ x
+minAbsorbLMax (pos zero) (pos y) = refl
+minAbsorbLMax (pos (suc x)) (pos zero) = cong sucℤ (minIdem (pos x))
+minAbsorbLMax (pos (suc x)) (pos (suc y))
+  = sym (sucDistMin (pos x) (max (pos x) (pos y))) ∙
+    cong sucℤ (minAbsorbLMax (pos x) (pos y))
+minAbsorbLMax (pos zero) (negsuc zero) = refl
+minAbsorbLMax (pos zero) (negsuc (suc y)) = refl
+minAbsorbLMax (pos (suc x)) (negsuc y) = cong sucℤ (minIdem (pos x))
+minAbsorbLMax (negsuc x) (pos y) = refl
+minAbsorbLMax (negsuc zero) (negsuc y) = refl
+minAbsorbLMax (negsuc (suc x)) (negsuc zero) = refl
+minAbsorbLMax (negsuc (suc x)) (negsuc (suc y))
+  = sym (predDistMin (negsuc x) (max (negsuc x) (negsuc y))) ∙
+    cong predℤ (minAbsorbLMax (negsuc x) (negsuc y))
+
+maxAbsorbLMin : ∀ x y → max x (min x y) ≡ x
+maxAbsorbLMin (pos zero) (pos y) = refl
+maxAbsorbLMin (pos (suc x)) (pos zero) = refl
+maxAbsorbLMin (pos (suc x)) (pos (suc y))
+  = sym (sucDistMax (pos x) (min (pos x) (pos y))) ∙
+    cong sucℤ (maxAbsorbLMin (pos x) (pos y))
+maxAbsorbLMin (pos zero) (negsuc y) = refl
+maxAbsorbLMin (pos (suc x)) (negsuc y) = refl
+maxAbsorbLMin (negsuc x) (pos y) = maxIdem (negsuc x)
+maxAbsorbLMin (negsuc zero) (negsuc y) = refl
+maxAbsorbLMin (negsuc (suc x)) (negsuc zero) = maxIdem (negsuc (suc x))
+maxAbsorbLMin (negsuc (suc x)) (negsuc (suc y))
+  = sym (predDistMax (negsuc x) (min (negsuc x) (negsuc y))) ∙
+    cong predℤ (maxAbsorbLMin (negsuc x) (negsuc y))
+
 injPos : ∀ {a b : ℕ} → pos a ≡ pos b → a ≡ b
 injPos {a} h = subst T h refl
   where
@@ -114,6 +408,12 @@ negsucNotpos a b h = subst T h 0
   T (pos _)    = ⊥
   T (negsuc _) = ℕ
 
+injNeg : ∀ {a b : ℕ} → neg a ≡ neg b → a ≡ b
+injNeg {zero} {zero} _ = refl
+injNeg {zero} {suc b} nega≡negb = ⊥.rec (posNotnegsuc 0 b nega≡negb)
+injNeg {suc a} {zero} nega≡negb = ⊥.rec (negsucNotpos a 0 nega≡negb)
+injNeg {suc a} {suc b} nega≡negb = cong suc (injNegsuc nega≡negb)
+
 discreteℤ : Discrete ℤ
 discreteℤ (pos n) (pos m) with discreteℕ n m
 ... | yes p = yes (cong pos p)
@@ -139,6 +439,18 @@ sucℤnegsucneg : ∀ n → sucℤ (negsuc n) ≡ neg n
 sucℤnegsucneg zero = refl
 sucℤnegsucneg (suc n) = refl
 
+-sucℤ : ∀ n → - sucℤ n ≡ predℤ (- n)
+-sucℤ (pos zero)       = refl
+-sucℤ (pos (suc n))    = refl
+-sucℤ (negsuc zero)    = refl
+-sucℤ (negsuc (suc n)) = refl
+
+-predℤ : ∀ n → - predℤ n ≡ sucℤ (- n)
+-predℤ (pos zero)       = refl
+-predℤ (pos (suc n))    = -pos n ∙ sym (sucℤnegsucneg n)
+-predℤ (negsuc zero)    = refl
+-predℤ (negsuc (suc n)) = refl
+
 -Involutive : ∀ z → - (- z) ≡ z
 -Involutive (pos n)    = cong -_ (-pos n) ∙ -neg n
 -Involutive (negsuc n) = refl
@@ -426,6 +738,70 @@ pos- (suc m) (suc n) =
    -  neg (suc n +ℕ suc m)     ≡⟨ pos+ (suc n) (suc m) ⟩
   (-  negsuc n) + (- negsuc m) ∎
 
+-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)) = -sucℤ (min (pos m) (pos n)) ∙
+                                       cong predℤ (-DistMin (pos m) (pos n)) ∙
+                                       predDistMax (- pos m) (- pos n) ∙
+                                       cong₂ max (sym (-sucℤ (pos m)))
+                                                 (sym (-sucℤ (pos n)))
+-DistMin (pos zero) (negsuc zero) = refl
+-DistMin (pos zero) (negsuc (suc n)) = refl
+-DistMin (pos (suc m)) (negsuc zero) = refl
+-DistMin (pos (suc m)) (negsuc (suc n)) = refl
+-DistMin (negsuc zero) (negsuc zero) = refl
+-DistMin (negsuc zero) (negsuc (suc n)) = refl
+-DistMin (negsuc (suc m)) (pos zero) = refl
+-DistMin (negsuc (suc m)) (pos (suc n)) = refl
+-DistMin (negsuc zero) (pos zero) = refl
+-DistMin (negsuc zero) (pos (suc n)) = refl
+-DistMin (negsuc (suc m)) (negsuc zero) = refl
+-DistMin (negsuc (suc m)) (negsuc (suc n)) = -predℤ (min (negsuc m) (negsuc n)) ∙
+                                             cong sucℤ (-DistMin (negsuc m) (negsuc n))
+
+-DistMax : ∀ m n → - max m n ≡ min (- m ) (- n)
+-DistMax (pos zero) (pos zero) = refl
+-DistMax (pos zero) (pos (suc n)) = refl
+-DistMax (pos (suc m)) (pos zero) = refl
+-DistMax (pos (suc m)) (pos (suc n)) = -sucℤ (max (pos m) (pos n)) ∙
+                                       cong predℤ (-DistMax (pos m) (pos n)) ∙
+                                       predDistMin (- pos m) (- pos n) ∙
+                                       cong₂ min (sym (-sucℤ (pos m)))
+                                                 (sym (-sucℤ (pos n)))
+-DistMax (pos zero) (negsuc zero) = refl
+-DistMax (pos zero) (negsuc (suc n)) = refl
+-DistMax (pos (suc m)) (negsuc zero) = refl
+-DistMax (pos (suc m)) (negsuc (suc n)) = refl
+-DistMax (negsuc zero) (pos zero) = refl
+-DistMax (negsuc zero) (pos (suc n)) = refl
+-DistMax (negsuc (suc m)) (pos zero) = refl
+-DistMax (negsuc (suc m)) (pos (suc n)) = refl
+-DistMax (negsuc zero) (negsuc zero) = refl
+-DistMax (negsuc zero) (negsuc (suc n)) = refl
+-DistMax (negsuc (suc m)) (negsuc zero) = refl
+-DistMax (negsuc (suc m)) (negsuc (suc n)) = -predℤ (max (negsuc m) (negsuc n)) ∙
+                                             cong sucℤ (-DistMax (negsuc m) (negsuc 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+ {pos zero} {l} {n} p = l            ≡⟨ pos0+ l ⟩
                               pos zero + l ≡⟨ p ⟩
@@ -451,6 +827,311 @@ inj-+z {z} {l} {n} p = inj-z+ {z = z} (+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)
 
+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) zero
+  = cong sucℤ (cong (λ a → min a (pos x)) (pos+ x 0) ∙ minIdem (pos x))
+pos+posLposMin (suc x) (suc y) = cong sucℤ (pos+posLposMin x (suc 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) zero
+  = cong sucℤ (cong (λ a → max a (pos x)) (pos+ x 0) ∙ maxIdem (pos x)) ∙
+    cong (pos ∘ suc) (sym (+-zero x))
+pos+posLposMax (suc x) (suc y) = cong sucℤ (pos+posLposMax x (suc 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 y)
+  = cong (λ a → min a (negsuc zero))
+         (sucℤ+ (negsuc zero) (pos y) ∙ sym (pos0+ (pos y))) ∙
+    minComm (pos y) (negsuc zero)
+negsuc+posLnegsucMin (suc x) zero = cong predℤ (minIdem (negsuc x))
+negsuc+posLnegsucMin (suc x) (suc y)
+  = cong (λ a → min a (negsuc (suc x)))
+         (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 y)
+  = cong (λ a → max a (negsuc zero))
+         (sucℤ+ (negsuc zero) (pos y) ∙ sym (pos0+ (pos y))) ∙
+    maxComm (pos y) (negsuc zero) ∙
+    pos0+ (pos y) ∙ sym (sucℤ+ (negsuc zero) (pos y))
+negsuc+posLnegsucMax (suc x) zero = cong predℤ (maxIdem (negsuc x))
+negsuc+posLnegsucMax (suc x) (suc y)
+  = cong (λ a → max a (negsuc (suc x)))
+         (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
+
+negsuc+negsucLposMin : ∀ x y z → min (negsuc x + negsuc y) (pos z) ≡ negsuc x + negsuc y
+negsuc+negsucLposMin x zero z = refl
+negsuc+negsucLposMin x (suc y) z
+  = cong (λ a → min a (pos z)) (predℤ+ (negsuc x) (negsuc y)) ∙
+    negsuc+negsucLposMin (suc x) y z ∙
+    sym (predℤ+ (negsuc x) (negsuc y))
+
+negsuc+negsucRposMin : ∀ x y z → min (pos x) (negsuc y + negsuc z) ≡ negsuc y + negsuc z
+negsuc+negsucRposMin z x y = minComm (pos z) (negsuc x + negsuc y) ∙ negsuc+negsucLposMin x y z
+
+negsuc+negsucLposMax : ∀ x y z → max (negsuc x + negsuc y) (pos z) ≡ pos z
+negsuc+negsucLposMax x zero z = refl
+negsuc+negsucLposMax x (suc y) z
+  = cong (λ a → max a (pos z))
+         (predℤ+ (negsuc x) (negsuc y)) ∙
+    negsuc+negsucLposMax (suc x) y z
+
+negsuc+negsucRposMax : ∀ x y z → max (pos x) (negsuc y + negsuc z) ≡ pos x
+negsuc+negsucRposMax z x y = maxComm (pos z) (negsuc x + negsuc y) ∙ negsuc+negsucLposMax x y z
+
+negsuc+negsucLnegsucMin : ∀ x y → min (negsuc x + negsuc y) (negsuc x) ≡ negsuc x + negsuc y
+negsuc+negsucLnegsucMin zero zero = refl
+negsuc+negsucLnegsucMin zero (suc y)
+  = cong (λ a → min a (negsuc zero))
+         (sym (predℤ+ (pos zero) (negsuc (suc y))) ∙
+          cong (predℤ ∘ predℤ) (sym (pos0+ (negsuc y)))) ∙
+    cong predℤ (cong predℤ (pos0+ (negsuc y)) ∙
+                predℤ+ (pos zero) (negsuc y))
+negsuc+negsucLnegsucMin (suc x) zero = cong predℤ (minPredL (negsuc x))
+negsuc+negsucLnegsucMin (suc x) (suc y)
+  = cong (λ a → min a (negsuc (suc x)))
+         (sym (predℤ+ (negsuc x) (negsuc (suc y)))) ∙
+    sym (predDistMin (negsuc x + negsuc (suc y)) (negsuc x)) ∙
+    cong predℤ (negsuc+negsucLnegsucMin x (suc y) ∙
+                predℤ+ (negsuc x) (negsuc 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)
+  = cong (λ a → max a (negsuc zero))
+         (sym (predℤ+ (pos zero) (negsuc (suc y))) ∙
+          cong (predℤ ∘ predℤ) (sym (pos0+ (negsuc y))))
+negsuc+negsucLnegsucMax (suc x) zero = cong predℤ (maxPredL (negsuc x))
+negsuc+negsucLnegsucMax (suc x) (suc y)
+  = cong (λ a → max a (negsuc (suc x)))
+         (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 zero zero = refl
+pos+pospos+negsucMin zero zero (suc z)
+  = cong (min (pos zero)) (+Comm (pos zero) (negsuc (suc z))) ∙
+    pos0+ (negsuc (suc z))
+pos+pospos+negsucMin zero (suc y) zero
+  = cong (λ a → min a (negsuc zero)) (+Comm (pos zero) (pos (suc y)))
+pos+pospos+negsucMin zero (suc y) (suc z)
+  = cong₂ min (+Comm (pos zero) (pos (suc y)))
+              (+Comm (pos zero) (negsuc (suc z))) ∙
+    pos0+ (negsuc (suc z))
+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 zero zero = refl
+pos+pospos+negsucMax zero zero (suc z) = cong (max (pos zero)) (sym (pos0+ (negsuc (suc z))))
+pos+pospos+negsucMax zero (suc y) zero
+  = cong (λ a → max a (negsuc zero))
+         (sym (pos0+ (pos (suc y)))) ∙
+    pos0+ (pos (suc y))
+pos+pospos+negsucMax zero (suc y) (suc z)
+  = cong₂ max (sym (pos0+ (pos (suc y))))
+          (sym (pos0+ (negsuc (suc z)))) ∙
+    pos0+ (pos (suc y))
+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 z)
+  = cong (min (negsuc 1))
+         (sucℤ+ (negsuc zero) (pos z) ∙ sym (pos0+ (pos z)))
+negsuc+negsucnegsuc+posMin zero (suc y) zero = negsuc+negsucLnegsucMin zero (suc y)
+negsuc+negsucnegsuc+posMin zero (suc y) (suc z)
+  = cong (min (negsuc zero + negsuc (suc y)))
+         (sucℤ+ (negsuc zero) (pos z) ∙ sym (pos0+ (pos z))) ∙
+    negsuc+negsucLposMin zero (suc y) z
+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 z)
+  = cong (max (negsuc 1))
+         (sucℤ+ (negsuc zero) (pos z) ∙
+          sym (pos0+ (pos z))) ∙
+    pos0+ (pos z) ∙
+    sym (sucℤ+ (negsuc zero) (pos z))
+negsuc+negsucnegsuc+posMax zero (suc y) zero = negsuc+negsucLnegsucMax zero (suc y)
+negsuc+negsucnegsuc+posMax zero (suc y) (suc z)
+  = cong (max (negsuc zero + negsuc (suc y)))
+         (sucℤ+ (negsuc zero) (pos z) ∙ sym (pos0+ (pos z))) ∙
+    negsuc+negsucLposMax zero (suc y) z ∙
+    pos0+ (pos z) ∙
+    sym (sucℤ+ (negsuc zero) (pos z))
+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 = sym (pos0+ (min y z)) ∙ cong₂ min (pos0+ y) (pos0+ z)
++DistRMin (pos (suc x)) (pos zero) (pos zero) = sym (cong sucℤ (minIdem (pos x)))
++DistRMin (pos (suc x)) (pos zero) (pos (suc z))
+  = cong sucℤ (+DistRMin (pos x) (pos zero) (pos (suc z))) ∙
+    sucDistMin (pos x) (pos x + pos (suc z)) ∙
+    cong (min (pos (suc x))) (sucℤ+ (pos x) (pos (suc z)))
++DistRMin (pos (suc x)) (pos (suc y)) (pos zero)
+  = cong sucℤ (+DistRMin (pos x) (pos (suc y)) (pos zero)) ∙
+    sucDistMin (pos x + pos (suc y)) (pos x) ∙
+    cong (λ a → min a (pos (suc x))) (sucℤ+ (pos x) (pos (suc y)))
++DistRMin (pos (suc x)) (pos (suc y)) (pos (suc z))
+  = sym (+sucℤ (pos (suc x)) (min (pos y) (pos z))) ∙
+    sucℤ+ (pos (suc x)) (min (pos y) (pos z)) ∙
+    +DistRMin (pos (suc (suc x))) (pos y) (pos z) ∙
+    cong₂ min (sym (sucℤ+ (pos (suc x)) (pos y)) ∙
+              +sucℤ (pos (suc x)) (pos y))
+              (sym (sucℤ+ (pos (suc x)) (pos z)) ∙
+              +sucℤ (pos (suc x)) (pos 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 (suc x) + negsuc y) (pos (suc x) + pos z) ∙
+         pos+pospos+negsucMin (suc x) z y)
++DistRMin (pos (suc x)) (negsuc zero) (negsuc zero) = sym (minIdem (pos x))
++DistRMin (pos (suc x)) (negsuc zero) (negsuc (suc z))
+  = (cong predℤ (sym (sucℤ+ (pos x) (negsuc z))) ∙
+     predSuc (pos x + negsuc z)) ∙
+     sym (pos+pospos+negsucMin x 0 z) ∙
+     cong (min (pos x)) (sym (predSuc (pos x + negsuc z)) ∙
+                         cong predℤ (sucℤ+ (pos x) (negsuc z)))
++DistRMin (pos (suc x)) (negsuc (suc y)) (negsuc zero)
+  = (cong predℤ (sym (sucℤ+ (pos x) (negsuc y))) ∙
+     predSuc (pos x + negsuc y)) ∙
+     sym (pos+pospos+negsucMin x 0 y) ∙
+     cong (min (pos x))
+          (sym (predSuc (pos x + negsuc y)) ∙
+          cong predℤ (sucℤ+ (pos x) (negsuc y))) ∙
+     minComm (pos x) (pos (suc x) + negsuc (suc y))
++DistRMin (pos (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = sym (+predℤ (pos (suc x)) (min (negsuc y) (negsuc z))) ∙
+    predℤ+ (pos (suc x)) (min (negsuc y) (negsuc z)) ∙
+    +DistRMin (pos x) (negsuc y) (negsuc z) ∙
+    cong₂ min (cong (_+ negsuc y) (sym (predSuc (pos x))) ∙
+               sym (predℤ+ (pos (suc x)) (negsuc y)))
+              (cong (_+ negsuc z) (sym (predSuc (pos x))) ∙
+               sym (predℤ+ (pos (suc x)) (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 y)) (pos (suc z))
+  = sym (+sucℤ (negsuc zero) (min (pos y) (pos z))) ∙
+    sucℤ+ (negsuc zero) (min (pos y) (pos z)) ∙
+    sym (pos0+ (min (pos y) (pos z))) ∙
+    cong₂ min (pos0+ (pos y) ∙ sym (sucℤ+ (negsuc zero) (pos y)))
+              (pos0+ (pos z) ∙ sym (sucℤ+ (negsuc zero) (pos z)))
++DistRMin (negsuc (suc x)) (pos (suc y)) (pos (suc 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)
++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))
+  = sym (cong (min (negsuc 1)) (predℤ+ (negsuc zero) (negsuc z)) ∙
+    negsuc+negsucRnegsucMin 1 z ∙
+    sym (predℤ+ (negsuc zero) (negsuc z)))
++DistRMin (negsuc zero) (negsuc (suc y)) (negsuc zero)
+  = sym (cong (λ a → min a (negsuc 1)) (predℤ+ (negsuc zero) (negsuc y)) ∙
+    negsuc+negsucLnegsucMin 1 y ∙
+    sym (predℤ+ (negsuc zero) (negsuc y)))
++DistRMin (negsuc zero) (negsuc (suc y)) (negsuc (suc z))
+  = sym (+predℤ (negsuc zero) (min (negsuc y) (negsuc z))) ∙
+    predℤ+ (negsuc zero) (min (negsuc y) (negsuc z)) ∙
+    +DistRMin (negsuc 1) (negsuc y) (negsuc z) ∙
+    cong₂ min (sym (predℤ+ (negsuc zero) (negsuc y)))
+              (sym (predℤ+ (negsuc zero) (negsuc z)))
++DistRMin (negsuc (suc x)) (negsuc zero) (negsuc zero)
+  = sym (cong (predℤ ∘ predℤ) (minIdem (negsuc x)))
++DistRMin (negsuc (suc x)) (negsuc zero) (negsuc (suc z))
+  = sym (sym (predDistMin (negsuc (suc x)) (negsuc (suc x) + negsuc z)) ∙
+         cong predℤ (negsuc+negsucRnegsucMin (suc x) z))
++DistRMin (negsuc (suc x)) (negsuc (suc y)) (negsuc zero)
+  = sym (sym (predDistMin (negsuc (suc x) + negsuc y) (negsuc (suc x))) ∙
+         cong predℤ (negsuc+negsucLnegsucMin (suc x) y))
++DistRMin (negsuc (suc x)) (negsuc (suc y)) (negsuc (suc z))
+  = 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)
+
++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)
 
 -- multiplication
 
@@ -500,8 +1181,17 @@ negsuc·negsuc (suc n) m = cong (pos (suc m) +_) (negsuc·negsuc n m)
 ·Comm (negsuc n) (negsuc m) =
   negsuc·negsuc n m ∙∙ ·Comm (pos (suc n)) (pos (suc m)) ∙∙ sym (negsuc·negsuc m n)
 
-·Rid : (x : ℤ) → x · 1 ≡ x
-·Rid x = ·Comm x 1
+·IdR : (x : ℤ) → x · 1 ≡ x
+·IdR x = ·Comm x 1
+
+·IdL : (x : ℤ) → 1 · x ≡ x
+·IdL x = refl
+
+·AnnihilR : (x : ℤ) → x · 0 ≡ 0
+·AnnihilR x = ·Comm x 0
+
+·AnnihilL : (x : ℤ) → 0 · x ≡ 0
+·AnnihilL x = refl
 
 private
   distrHelper : (x y z w : ℤ) → (x + y) + (z + w) ≡ ((x + z) + (y + w))
@@ -562,6 +1252,165 @@ private
   ∙∙ cong (_+ ((negsuc n · b) · c)) (-DistL· b c)
   ∙∙ sym (·DistL+ (- b) (negsuc n · b) c)
 
+·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ℤ· : (a b : ℤ) → sucℤ a · b ≡ b + a · b
+sucℤ· (pos a) (pos b) = refl
+sucℤ· (pos a) (negsuc b) = refl
+sucℤ· (negsuc zero) (pos b) = sym (-Cancel (pos b))
+sucℤ· (negsuc (suc a)) (pos b) =
+  negsuc a · pos b                     ≡⟨ pos0+ (negsuc a · pos b) ⟩
+  pos zero + negsuc a · pos b          ≡⟨ cong (_+ negsuc a · pos b) (sym (-Cancel (pos b))) ⟩
+  pos b + - pos b + negsuc a · pos b   ≡⟨ sym (+Assoc (pos b) (- pos b) (negsuc a · pos b)) ⟩
+  pos b + (- pos b + negsuc a · pos b) ∎
+sucℤ· (negsuc zero) (negsuc b) =
+      pos zero                ≡⟨ sym (-Cancel' (pos b)) ⟩
+  ((- pos b) +pos b)          ≡⟨ cong (_+pos b) (-pos b) ⟩
+     (neg b  +pos b)          ≡⟨ cong (_+pos b) (sym (sucℤnegsucneg b)) ⟩
+     (sucℤ (negsuc b) +pos b) ≡⟨ sym (sucℤ+pos b (negsuc b)) ⟩
+      sucℤ (negsuc b  +pos b) ∎
+sucℤ· (negsuc (suc a)) (negsuc b) =
+  negsuc a · negsuc b                              ≡⟨ pos0+ (negsuc a · negsuc b) ⟩
+  pos zero + negsuc a · negsuc b                   ≡⟨ cong (_+ negsuc a · negsuc b) (sym (-Cancel' (pos (suc b)))) ⟩
+ (negsuc b + (pos (suc b))) + negsuc a · negsuc b  ≡⟨ sym (+Assoc (negsuc b) (pos (suc b)) (negsuc a · negsuc b)) ⟩
+  negsuc b + (pos (suc b)   + negsuc a · negsuc 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ℤ· : (a  b : ℤ) → predℤ a · b ≡ - b + a · b
+predℤ· (pos zero) b = refl
+predℤ· (pos (suc a)) b
+  = pos0+ (pos a · b) ∙
+    cong (_+ pos a · b) (sym (-Cancel' b)) ∙
+    sym (+Assoc (- b) b (pos a · b))
+predℤ· (negsuc a) b = refl
+
+·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 = refl
+·DistPosRMin (suc x) (pos zero) (pos zero)
+  = ·Comm (pos (suc x)) (pos zero) ∙
+    cong₂ min (·Comm (pos zero) (pos (suc x)))
+              (·Comm (pos zero) (pos (suc x)))
+·DistPosRMin (suc x) (pos zero) (pos (suc z))
+  = ·Comm (pos (suc x)) (pos zero) ∙
+    cong₂ min (·Comm (pos zero) (pos (suc x)))
+              (pos·pos (suc x) (suc z))
+·DistPosRMin (suc x) (pos (suc y)) (pos zero)
+  = ·Comm (pos (suc x)) (pos zero) ∙
+    cong₂ min (pos·pos (suc x) (suc y))
+              (·Comm (pos zero) (pos (suc x)))
+·DistPosRMin (suc x) (pos (suc y)) (pos (suc z))
+  = ·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))
+  = ·predℤ (pos (suc x)) (negsuc z) ∙
+    cong (_- pos (suc x)) (·DistPosRMin (suc x) (pos zero) (negsuc z)) ∙
+    +DistLMin (pos (suc x) · pos zero) (pos (suc x) · negsuc z) (- pos (suc x)) ∙
+    cong₂ min (cong (_+ negsuc x) (·AnnihilR (pos (suc x))) ∙
+               sym (pos0+ (negsuc x)) ∙
+               ·Comm (negsuc zero) (pos (suc x)))
+              (sym (·predℤ (pos (suc x)) (negsuc z)))
+·DistPosRMin (suc x) (negsuc (suc y)) (negsuc zero)
+  = ·predℤ (pos (suc x)) (negsuc y) ∙
+    cong (_- pos (suc x)) (·DistPosRMin (suc x) (negsuc y) (pos zero)) ∙
+    +DistLMin (pos (suc x) · negsuc y) (pos (suc x) · pos zero) (- pos (suc x)) ∙
+    cong₂ min (sym (·predℤ (pos (suc x)) (negsuc y)))
+              (cong (_+ negsuc x) (·AnnihilR (pos (suc x))) ∙
+               sym (pos0+ (negsuc x)) ∙
+               ·Comm (negsuc zero) (pos (suc x)))
+·DistPosRMin (suc x) (negsuc (suc y)) (negsuc (suc z))
+  = ·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- x = +Comm (- x) 0
 
diff --git a/Cubical/Data/Rationals/Base.agda b/Cubical/Data/Rationals/Base.agda
index a16ea8d95f..550a21045b 100644
--- a/Cubical/Data/Rationals/Base.agda
+++ b/Cubical/Data/Rationals/Base.agda
@@ -3,11 +3,12 @@ module Cubical.Data.Rationals.Base where
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
 
 open import Cubical.Data.Nat as ℕ using (discreteℕ)
 open import Cubical.Data.NatPlusOne
 open import Cubical.Data.Sigma
-open import Cubical.Data.Int.MoreInts.QuoInt
+open import Cubical.Data.Int
 
 open import Cubical.HITs.SetQuotients as SetQuotient
   using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public
@@ -19,10 +20,6 @@ open BinaryRelation
 ℕ₊₁→ℤ : ℕ₊₁ → ℤ
 ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n)
 
-private
-  ℕ₊₁→ℤ-hom : ∀ m n → ℕ₊₁→ℤ (m ·₊₁ n) ≡ ℕ₊₁→ℤ m · ℕ₊₁→ℤ n
-  ℕ₊₁→ℤ-hom _ _ = refl
-
 
 -- ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)
 
@@ -43,16 +40,16 @@ isSetℚ = SetQuotient.squash/
 isEquivRel∼ : isEquivRel _∼_
 isEquivRel.reflexive isEquivRel∼ (a , b) = refl
 isEquivRel.symmetric isEquivRel∼ (a , b) (c , d) = sym
-isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·-injʳ _ _ _ r
-  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·-comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
-            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·-assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
+isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·rCancel _ _ (e · pos (ℕ.suc (ℕ₊₁.n b))) r (ℕ.snotz ∘ injPos)
+  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·Comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
+            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·Assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
             ℕ₊₁→ℤ f · (a · ℕ₊₁→ℤ d) ≡[ i ]⟨ ℕ₊₁→ℤ f · p i ⟩
-            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·-assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
-            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·-comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
+            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·Assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
+            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·Comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
             (c · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ b ≡[ i ]⟨ q i · ℕ₊₁→ℤ b ⟩
-            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·-assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
-            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·-comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
-            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·-assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
+            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
+            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
             (e · ℕ₊₁→ℤ b) · ℕ₊₁→ℤ d ∎
 
 eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y
diff --git a/Cubical/Data/Rationals/MoreRationals/QuoQ.agda b/Cubical/Data/Rationals/MoreRationals/QuoQ.agda
new file mode 100644
index 0000000000..fc20a7fa8e
--- /dev/null
+++ b/Cubical/Data/Rationals/MoreRationals/QuoQ.agda
@@ -0,0 +1,6 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.QuoQ where
+
+open import Cubical.Data.Rationals.MoreRationals.QuoQ.Base public
+
+open import Cubical.Data.Rationals.MoreRationals.QuoQ.Properties public
diff --git a/Cubical/Data/Rationals/MoreRationals/QuoQ/Base.agda b/Cubical/Data/Rationals/MoreRationals/QuoQ/Base.agda
new file mode 100644
index 0000000000..02b04dde9d
--- /dev/null
+++ b/Cubical/Data/Rationals/MoreRationals/QuoQ/Base.agda
@@ -0,0 +1,75 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.QuoQ.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+
+open import Cubical.Data.Nat as ℕ using (discreteℕ)
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Sigma
+open import Cubical.Data.Int.MoreInts.QuoInt
+
+open import Cubical.HITs.SetQuotients as SetQuotient
+  using ([_]; eq/; discreteSetQuotients) renaming (_/_ to _//_) public
+
+open import Cubical.Relation.Nullary
+open import Cubical.Relation.Binary.Base
+open BinaryRelation
+
+ℕ₊₁→ℤ : ℕ₊₁ → ℤ
+ℕ₊₁→ℤ n = pos (ℕ₊₁→ℕ n)
+
+private
+  ℕ₊₁→ℤ-hom : ∀ m n → ℕ₊₁→ℤ (m ·₊₁ n) ≡ ℕ₊₁→ℤ m · ℕ₊₁→ℤ n
+  ℕ₊₁→ℤ-hom _ _ = refl
+
+
+-- ℚ as a set quotient of ℤ × ℕ₊₁ (as in the HoTT book)
+
+_∼_ : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → Type₀
+(a , b) ∼ (c , d) = a · ℕ₊₁→ℤ d ≡ c · ℕ₊₁→ℤ b
+
+ℚ : Type₀
+ℚ = (ℤ × ℕ₊₁) // _∼_
+
+
+isSetℚ : isSet ℚ
+isSetℚ = SetQuotient.squash/
+
+[_/_] : ℤ → ℕ₊₁ → ℚ
+[ a / b ] = [ a , b ]
+
+
+isEquivRel∼ : isEquivRel _∼_
+isEquivRel.reflexive isEquivRel∼ (a , b) = refl
+isEquivRel.symmetric isEquivRel∼ (a , b) (c , d) = sym
+isEquivRel.transitive isEquivRel∼ (a , b) (c , d) (e , f) p q = ·-injʳ _ _ _ r
+  where r = (a · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ d ≡[ i ]⟨ ·-comm a (ℕ₊₁→ℤ f) i · ℕ₊₁→ℤ d ⟩
+            (ℕ₊₁→ℤ f · a) · ℕ₊₁→ℤ d ≡⟨ sym (·-assoc (ℕ₊₁→ℤ f) a (ℕ₊₁→ℤ d)) ⟩
+            ℕ₊₁→ℤ f · (a · ℕ₊₁→ℤ d) ≡[ i ]⟨ ℕ₊₁→ℤ f · p i ⟩
+            ℕ₊₁→ℤ f · (c · ℕ₊₁→ℤ b) ≡⟨ ·-assoc (ℕ₊₁→ℤ f) c (ℕ₊₁→ℤ b) ⟩
+            (ℕ₊₁→ℤ f · c) · ℕ₊₁→ℤ b ≡[ i ]⟨ ·-comm (ℕ₊₁→ℤ f) c i · ℕ₊₁→ℤ b ⟩
+            (c · ℕ₊₁→ℤ f) · ℕ₊₁→ℤ b ≡[ i ]⟨ q i · ℕ₊₁→ℤ b ⟩
+            (e · ℕ₊₁→ℤ d) · ℕ₊₁→ℤ b ≡⟨ sym (·-assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+            e · (ℕ₊₁→ℤ d · ℕ₊₁→ℤ b) ≡[ i ]⟨ e · ·-comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) i ⟩
+            e · (ℕ₊₁→ℤ b · ℕ₊₁→ℤ d) ≡⟨ ·-assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ⟩
+            (e · ℕ₊₁→ℤ b) · ℕ₊₁→ℤ d ∎
+
+eq/⁻¹ : ∀ x y → Path ℚ [ x ] [ y ] → x ∼ y
+eq/⁻¹ = SetQuotient.effective (λ _ _ → isSetℤ _ _) isEquivRel∼
+
+discreteℚ : Discrete ℚ
+discreteℚ = discreteSetQuotients isEquivRel∼ (λ _ _ → discreteℤ _ _)
+
+
+-- Natural number and negative integer literals for ℚ
+
+open import Cubical.Data.Nat.Literals public
+
+instance
+  fromNatℚ : HasFromNat ℚ
+  fromNatℚ = record { Constraint = λ _ → Unit ; fromNat = λ n → [ pos n / 1 ] }
+
+instance
+  fromNegℚ : HasFromNeg ℚ
+  fromNegℚ = record { Constraint = λ _ → Unit ; fromNeg = λ n → [ neg n / 1 ] }
diff --git a/Cubical/Data/Rationals/MoreRationals/QuoQ/Properties.agda b/Cubical/Data/Rationals/MoreRationals/QuoQ/Properties.agda
new file mode 100644
index 0000000000..a29613bf4e
--- /dev/null
+++ b/Cubical/Data/Rationals/MoreRationals/QuoQ/Properties.agda
@@ -0,0 +1,248 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.MoreRationals.QuoQ.Properties where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.GroupoidLaws hiding (_⁻¹)
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Data.Int.MoreInts.QuoInt as ℤ using (ℤ; Sign; signed; pos; neg; posneg; sign)
+open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)
+
+open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Sigma
+
+open import Cubical.Data.Sum
+open import Cubical.Relation.Nullary
+
+open import Cubical.Data.Rationals.MoreRationals.QuoQ.Base
+
+ℚ-cancelˡ : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.· a / c ·₊₁ b ] ≡ [ a / b ]
+ℚ-cancelˡ {a} {b} c = eq/ _ _
+  (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.·-comm (ℕ₊₁→ℤ c) a) ∙ sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))
+
+ℚ-cancelʳ : ∀ {a b} (c : ℕ₊₁) → [ a ℤ.· ℕ₊₁→ℤ c / b ·₊₁ c ] ≡ [ a / b ]
+ℚ-cancelʳ {a} {b} c = eq/ _ _
+  (sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ∙ cong (a ℤ.·_) (ℤ.·-comm (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))
+
+-- useful functions for defining operations on ℚ
+
+onCommonDenom :
+  (g : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ)
+  (g-eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+           → ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) ≡ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)))
+  (g-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
+           → (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d)
+  → ℚ → ℚ → ℚ
+onCommonDenom g g-eql g-eqr = SetQuotient.rec2 isSetℚ
+  (λ { (a , b) (c , d) → [ g (a , b) (c , d) / b ·₊₁ d ] })
+  (λ { (a , b) (c , d) (e , f) p → eql (a , b) (c , d) (e , f) p })
+  (λ { (a , b) (c , d) (e , f) p → eqr (a , b) (c , d) (e , f) p })
+  where eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+              → [ g (a , b) (e , f) / b ·₊₁ f ] ≡ [ g (c , d) (e , f) / d ·₊₁ f ]
+        eql (a , b) (c , d) (e , f) p =
+          [ g (a , b) (e , f) / b ·₊₁ f ]
+            ≡⟨ sym (ℚ-cancelˡ d) ⟩
+          [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / d ·₊₁ (b ·₊₁ f) ]
+            ≡[ i ]⟨ [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / ·₊₁-assoc d b f i ] ⟩
+          [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / (d ·₊₁ b) ·₊₁ f ]
+            ≡[ i ]⟨ [ g-eql (a , b) (c , d) (e , f) p i / ·₊₁-comm d b i ·₊₁ f ] ⟩
+          [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / (b ·₊₁ d) ·₊₁ f ]
+            ≡[ i ]⟨ [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / ·₊₁-assoc b d f (~ i) ] ⟩
+          [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / b ·₊₁ (d ·₊₁ f) ]
+            ≡⟨ ℚ-cancelˡ b ⟩
+          [ g (c , d) (e , f) / d ·₊₁ f ] ∎
+        eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
+             → [ g (a , b) (c , d) / b ·₊₁ d ] ≡ [ g (a , b) (e , f) / b ·₊₁ f ]
+        eqr (a , b) (c , d) (e , f) p =
+          [ g (a , b) (c , d) / b ·₊₁ d ]
+            ≡⟨ sym (ℚ-cancelʳ f) ⟩
+          [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / (b ·₊₁ d) ·₊₁ f ]
+            ≡[ i ]⟨ [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / ·₊₁-assoc b d f (~ i) ] ⟩
+          [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / b ·₊₁ (d ·₊₁ f) ]
+            ≡[ i ]⟨ [ g-eqr (a , b) (c , d) (e , f) p i / b ·₊₁ ·₊₁-comm d f i ] ⟩
+          [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / b ·₊₁ (f ·₊₁ d) ]
+            ≡[ i ]⟨ [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / ·₊₁-assoc b f d i ] ⟩
+          [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / (b ·₊₁ f) ·₊₁ d ]
+            ≡⟨ ℚ-cancelʳ d ⟩
+          [ g (a , b) (e , f) / b ·₊₁ f ] ∎
+
+onCommonDenomSym :
+  (g : ℤ × ℕ₊₁ → ℤ × ℕ₊₁ → ℤ)
+  (g-sym : ∀ x y → g x y ≡ g y x)
+  (g-eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+           → ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) ≡ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)))
+  → ℚ → ℚ → ℚ
+onCommonDenomSym g g-sym g-eql = onCommonDenom g g-eql q-eqr
+  where q-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
+                → (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d
+        q-eqr (a , b) (c , d) (e , f) p =
+          (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡[ i ]⟨ ℤ.·-comm (g-sym (a , b) (c , d) i) (ℕ₊₁→ℤ f) i ⟩
+          ℕ₊₁→ℤ f ℤ.· (g (c , d) (a , b)) ≡⟨ g-eql (c , d) (e , f) (a , b) p ⟩
+          ℕ₊₁→ℤ d ℤ.· (g (e , f) (a , b)) ≡[ i ]⟨ ℤ.·-comm (ℕ₊₁→ℤ d) (g-sym (e , f) (a , b) i) i ⟩
+          (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d ∎
+
+onCommonDenomSym-comm : ∀ {g} g-sym {g-eql} (x y : ℚ)
+                        → onCommonDenomSym g g-sym g-eql x y ≡
+                          onCommonDenomSym g g-sym g-eql y x
+onCommonDenomSym-comm g-sym = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) i → [ g-sym (a , b) (c , d) i / ·₊₁-comm b d i ] })
+
+
+-- basic arithmetic operations on ℚ
+
+infixl 6 _+_
+infixl 7 _·_
+
+private
+  lem₁ : ∀ a b c d e (p : a ℤ.· b ≡ c ℤ.· d) → b ℤ.· (a ℤ.· e) ≡ d ℤ.· (c ℤ.· e)
+  lem₁ a b c d e p =   ℤ.·-assoc b a e
+                     ∙ cong (ℤ._· e) (ℤ.·-comm b a ∙ p ∙ ℤ.·-comm c d)
+                     ∙ sym (ℤ.·-assoc d c e)
+
+  lem₂ : ∀ a b c → a ℤ.· (b ℤ.· c) ≡ c ℤ.· (b ℤ.· a)
+  lem₂ a b c =   cong (a ℤ.·_) (ℤ.·-comm b c) ∙ ℤ.·-assoc a c b
+               ∙ cong (ℤ._· b) (ℤ.·-comm a c) ∙ sym (ℤ.·-assoc c a b)
+               ∙ cong (c ℤ.·_) (ℤ.·-comm a b)
+
+_+_ : ℚ → ℚ → ℚ
+_+_ = onCommonDenomSym
+  (λ { (a , b) (c , d) → a ℤ.· (ℕ₊₁→ℤ d) ℤ.+ c ℤ.· (ℕ₊₁→ℤ b) })
+  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
+  (λ { (a , b) (c , d) (e , f) p →
+    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ b)
+      ≡⟨ sym (ℤ.·-distribˡ (ℕ₊₁→ℤ d) (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b)) ⟩
+    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b)
+      ≡[ i ]⟨ lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) p i ℤ.+ lem₂ (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b) i ⟩
+    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d)
+      ≡⟨ ℤ.·-distribˡ (ℕ₊₁→ℤ b) (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) ⟩
+    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ∎ })
+
++-comm : ∀ x y → x + y ≡ y + x
++-comm = onCommonDenomSym-comm
+  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
+
++-identityˡ : ∀ x → 0 + x ≡ x
++-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityˡ b i ] })
+
++-identityʳ : ∀ x → x + 0 ≡ x
++-identityʳ x = +-comm x _ ∙ +-identityˡ x
+
++-assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
++-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) i → [ eq a (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ f) i / ·₊₁-assoc b d f i ] })
+  where eq₁ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ a ℤ.· (c ℤ.· b)
+        eq₁ a b c = sym (ℤ.·-assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·-comm b c)
+        eq₂ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ (a ℤ.· c) ℤ.· b
+        eq₂ a b c = eq₁ a b c ∙ ℤ.·-assoc a c b
+
+        eq : ∀ a b c d e f → Path ℤ _ _
+        eq a b c d e f =
+          a ℤ.· (d ℤ.· f) ℤ.+ (c ℤ.· f ℤ.+ e ℤ.· d) ℤ.· b
+            ≡[ i ]⟨ a ℤ.· (d ℤ.· f) ℤ.+ ℤ.·-distribʳ (c ℤ.· f) (e ℤ.· d) b (~ i) ⟩
+          a ℤ.· (d ℤ.· f) ℤ.+ ((c ℤ.· f) ℤ.· b ℤ.+ (e ℤ.· d) ℤ.· b)
+            ≡[ i ]⟨ ℤ.+-assoc (ℤ.·-assoc a d f i) (eq₂ c f b i) (eq₁ e d b i) i ⟩
+          ((a ℤ.· d) ℤ.· f ℤ.+ (c ℤ.· b) ℤ.· f) ℤ.+ e ℤ.· (b ℤ.· d)
+            ≡[ i ]⟨ ℤ.·-distribʳ (a ℤ.· d) (c ℤ.· b) f i ℤ.+ e ℤ.· (b ℤ.· d) ⟩
+          (a ℤ.· d ℤ.+ c ℤ.· b) ℤ.· f ℤ.+ e ℤ.· (b ℤ.· d) ∎
+
+
+_·_ : ℚ → ℚ → ℚ
+_·_ = onCommonDenomSym
+  (λ { (a , _) (c , _) → a ℤ.· c })
+  (λ { (a , _) (c , _) → ℤ.·-comm a c })
+  (λ { (a , b) (c , d) (e , _) p → lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) e p })
+
+·-comm : ∀ x y → x · y ≡ y · x
+·-comm = onCommonDenomSym-comm (λ { (a , _) (c , _) → ℤ.·-comm a c })
+
+·-identityˡ : ∀ x → 1 · x ≡ x
+·-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) i → [ ℤ.·-identityˡ a i / ·₊₁-identityˡ b i ] })
+
+·-identityʳ : ∀ x → x · 1 ≡ x
+·-identityʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityʳ b i ] })
+
+·-zeroˡ : ∀ x → 0 · x ≡ 0
+·-zeroˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) → (λ i → [ p a b i / 1 ·₊₁ b ]) ∙ ℚ-cancelʳ b })
+  where p : ∀ a b → 0 ℤ.· a ≡ 0 ℤ.· ℕ₊₁→ℤ b
+        p a b = ℤ.·-zeroˡ {ℤ.spos} a ∙ sym (ℤ.·-zeroˡ {ℤ.spos} (ℕ₊₁→ℤ b))
+
+·-zeroʳ : ∀ x → x · 0 ≡ 0
+·-zeroʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) → (λ i → [ p a b i / b ·₊₁ 1 ]) ∙ ℚ-cancelˡ b })
+  where p : ∀ a b → a ℤ.· 0 ≡ ℕ₊₁→ℤ b ℤ.· 0
+        p a b = ℤ.·-zeroʳ {ℤ.spos} a ∙ sym (ℤ.·-zeroʳ {ℤ.spos} (ℕ₊₁→ℤ b))
+
+·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
+·-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) i → [ ℤ.·-assoc a c e i / ·₊₁-assoc b d f i ] })
+
+·-distribˡ : ∀ x y z → (x · y) + (x · z) ≡ x · (y + z)
+·-distribˡ = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) → eq a b c d e f })
+  where lem : ∀ {ℓ} {A : Type ℓ} (_·_ : A → A → A)
+                (·-comm : ∀ x y → x · y ≡ y · x)
+                (·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z)
+                a c b d
+              → (a · c) · (b · d) ≡ (a · (c · d)) · b
+        lem _·_ ·-comm ·-assoc a c b d =
+          (a · c) · (b · d) ≡[ i ]⟨ (a · c) · ·-comm b d i ⟩
+          (a · c) · (d · b) ≡⟨ ·-assoc (a · c) d b ⟩
+          ((a · c) · d) · b ≡[ i ]⟨ ·-assoc a c d (~ i) · b ⟩
+          (a · (c · d)) · b ∎
+
+        lemℤ   = lem ℤ._·_ ℤ.·-comm ℤ.·-assoc
+        lemℕ₊₁ = lem _·₊₁_ ·₊₁-comm ·₊₁-assoc
+
+        eq : ∀ a b c d e f →
+               [ (a ℤ.· c) ℤ.· ℕ₊₁→ℤ (b ·₊₁ f) ℤ.+ (a ℤ.· e) ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)
+                 / (b ·₊₁ d) ·₊₁ (b ·₊₁ f) ]
+             ≡ [ a ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d)
+                / b ·₊₁ (d ·₊₁ f) ]
+        eq a b c d e f =
+          (λ i → [ lemℤ a c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) i ℤ.+ lemℤ a e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) i
+                   / lemℕ₊₁ b d b f i ]) ∙
+          (λ i → [ ℤ.·-distribʳ (a ℤ.· (c ℤ.· ℕ₊₁→ℤ f)) (a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)) (ℕ₊₁→ℤ b) i
+                   / (b ·₊₁ (d ·₊₁ f)) ·₊₁ b ]) ∙
+          ℚ-cancelʳ {a ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)} {b ·₊₁ (d ·₊₁ f)} b ∙
+          (λ i → [ ℤ.·-distribˡ a (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) i
+                   / b ·₊₁ (d ·₊₁ f) ])
+
+·-distribʳ : ∀ x y z → (x · z) + (y · z) ≡ (x + y) · z
+·-distribʳ x y z = (λ i → ·-comm x z i + ·-comm y z i) ∙ ·-distribˡ z x y ∙ ·-comm z (x + y)
+
+
+-_ : ℚ → ℚ
+- x = -1 · x
+
+negate-invol : ∀ x → - - x ≡ x
+negate-invol x = ·-assoc -1 -1 x ∙ ·-identityˡ x
+
+negateEquiv : ℚ ≃ ℚ
+negateEquiv = isoToEquiv (iso -_ -_ negate-invol negate-invol)
+
+negateEq : ℚ ≡ ℚ
+negateEq = ua negateEquiv
+
++-inverseˡ : ∀ x → (- x) + x ≡ 0
++-inverseˡ x = (λ i → (-1 · x) + ·-identityˡ x (~ i)) ∙ ·-distribʳ -1 1 x ∙ ·-zeroˡ x
+
+_-_ : ℚ → ℚ → ℚ
+x - y = x + (- y)
+
++-inverseʳ : ∀ x → x - x ≡ 0
++-inverseʳ x = +-comm x (- x) ∙ +-inverseˡ x
+
++-injˡ : ∀ x y z → x + y ≡ x + z → y ≡ z
++-injˡ x y z p = sym (q y) ∙ cong ((- x) +_) p ∙ q z
+  where q : ∀ y → (- x) + (x + y) ≡ y
+        q y = +-assoc (- x) x y ∙ cong (_+ y) (+-inverseˡ x) ∙ +-identityˡ y
+
++-injʳ : ∀ x y z → x + y ≡ z + y → x ≡ z
++-injʳ x y z p = +-injˡ y x z (+-comm y x ∙ p ∙ +-comm z y)
diff --git a/Cubical/Data/Rationals/MoreRationals/SigmaQ/Properties.agda b/Cubical/Data/Rationals/MoreRationals/SigmaQ/Properties.agda
index 84ee4adae7..718a367bc0 100644
--- a/Cubical/Data/Rationals/MoreRationals/SigmaQ/Properties.agda
+++ b/Cubical/Data/Rationals/MoreRationals/SigmaQ/Properties.agda
@@ -17,7 +17,7 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.Nat.GCD
 open import Cubical.Data.Nat.Coprime
 
-open import Cubical.Data.Rationals as Quo using (ℕ₊₁→ℤ)
+open import Cubical.Data.Rationals.MoreRationals.QuoQ as Quo using (ℕ₊₁→ℤ)
 import Cubical.Data.Rationals.MoreRationals.SigmaQ.Base as Sigma
 
 
diff --git a/Cubical/Data/Rationals/Order.agda b/Cubical/Data/Rationals/Order.agda
new file mode 100644
index 0000000000..a18910dbec
--- /dev/null
+++ b/Cubical/Data/Rationals/Order.agda
@@ -0,0 +1,623 @@
+{-# OPTIONS --safe #-}
+module Cubical.Data.Rationals.Order where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Functions.Logic using (_⊔′_)
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Int.Base as ℤ using (ℤ)
+open import Cubical.Data.Int.Properties as ℤ using ()
+open import Cubical.Data.Int.Order as ℤ using ()
+open import Cubical.Data.Rationals.Base as ℚ
+open import Cubical.Data.Rationals.Properties as ℚ
+open import Cubical.Data.Nat as ℕ
+open import Cubical.Data.NatPlusOne
+open import Cubical.Data.Sigma
+open import Cubical.Data.Sum as ⊎ using (_⊎_; inl; inr; isProp⊎)
+
+open import Cubical.HITs.PropositionalTruncation as ∥₁ using (isPropPropTrunc; ∣_∣₁)
+open import Cubical.HITs.SetQuotients
+
+open import Cubical.Relation.Nullary
+open import Cubical.Relation.Binary.Base
+
+infix 4 _≤_ _<_ _≥_ _>_
+
+private
+  ·CommR : (a b c : ℤ) → a ℤ.· b ℤ.· c ≡ a ℤ.· c ℤ.· b
+  ·CommR a b c = sym (ℤ.·Assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·Comm b c) ∙ ℤ.·Assoc a c b
+
+  _≤'_ : ℚ → ℚ → hProp ℓ-zero
+  _≤'_ = fun
+    where
+        lemma≤ : ((a , b) (c , d) (e , f) : (ℤ × ℕ₊₁))
+                → (c ℤ.· ℕ₊₁→ℤ f ) ≡ (e ℤ.· ℕ₊₁→ℤ d)
+                → ((a ℤ.· ℕ₊₁→ℤ d) ℤ.≤ (c ℤ.· ℕ₊₁→ℤ b))
+                ≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.≤ (e ℤ.· ℕ₊₁→ℤ b))
+        lemma≤ (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤
+                (ℤ.≤-·o-cancel {k = -1+ d} ∘
+                  subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                               (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙
+                                cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙
+                                ·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.≤-·o {k = ℕ₊₁→ℕ f})
+                (ℤ.≤-·o-cancel {k = -1+ f} ∘
+                  subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d))
+                                (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙
+                                 cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙
+                                 ·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.≤-·o {k = ℕ₊₁→ℕ d})))
+
+        fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero
+        fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.≤ c ℤ.· ℕ₊₁→ℤ b
+        snd (fun₀ _ [ _ ]) = ℤ.isProp≤
+        fun₀ a/b (eq/ c/d e/f cf≡ed i) = record
+          { fst = lemma≤ a/b c/d e/f cf≡ed i
+          ; snd = isProp→PathP (λ i → isPropIsProp {A = lemma≤ a/b c/d e/f cf≡ed i}) ℤ.isProp≤ ℤ.isProp≤ i
+          }
+        fun₀ a/b (squash/ x y p q i j) = isSet→SquareP (λ _ _ → isSetHProp)
+          (λ _ → fun₀ a/b x)
+          (λ _ → fun₀ a/b y)
+          (λ i → fun₀ a/b (p i))
+          (λ i → fun₀ a/b (q i)) j i
+
+        toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y
+        toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) →
+          Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp≤ ℤ.isProp≤
+                (ℤ.≤-·o-cancel {k = -1+ b} ∘
+                  subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙
+                                 cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙
+                                 ·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                               (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘
+                 ℤ.≤-·o {k = ℕ₊₁→ℕ d})
+                (ℤ.≤-·o-cancel {k = -1+ d} ∘
+                  subst2 ℤ._≤_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙
+                                 cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙
+                                 ·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                               (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.≤-·o {k = ℕ₊₁→ℕ b})))
+
+        fun : ℚ → ℚ → hProp ℓ-zero
+        fun [ a/b ] y = fun₀ a/b y
+        fun (eq/ a/b c/d ad≡cb i) y = toPath a/b c/d ad≡cb y i
+        fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → isSetHProp)
+          (λ _ → fun x z) (λ _ → fun y z) (λ i → fun (p i) z) (λ i → fun (q i) z) j i
+
+  _<'_ : ℚ → ℚ → hProp ℓ-zero
+  _<'_ = fun
+    where
+        lemma< : ((a , b) (c , d) (e , f) : (ℤ × ℕ₊₁))
+                → (c ℤ.· ℕ₊₁→ℤ f ) ≡ (e ℤ.· ℕ₊₁→ℤ d)
+                → ((a ℤ.· ℕ₊₁→ℤ d) ℤ.< (c ℤ.· ℕ₊₁→ℤ b))
+                ≡ ((a ℤ.· ℕ₊₁→ℤ f) ℤ.< (e ℤ.· ℕ₊₁→ℤ b))
+        lemma< (a , b) (c , d) (e , f) cf≡ed = (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp<
+                (ℤ.<-·o-cancel {k = -1+ d} ∘
+                  subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                               (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) ∙
+                                cong (ℤ._· ℕ₊₁→ℤ b) cf≡ed ∙
+                                ·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.<-·o {k = -1+ f})
+                (ℤ.<-·o-cancel {k = -1+ f} ∘
+                  subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d))
+                               (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) ∙
+                                cong (ℤ._· ℕ₊₁→ℤ b) (sym cf≡ed) ∙
+                                ·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.<-·o {k = -1+ d})))
+
+        fun₀ : ℤ × ℕ₊₁ → ℚ → hProp ℓ-zero
+        fst (fun₀ (a , b) [ c , d ]) = a ℤ.· ℕ₊₁→ℤ d ℤ.< c ℤ.· ℕ₊₁→ℤ b
+        snd (fun₀ _ [ _ ]) = ℤ.isProp<
+        fun₀ a/b (eq/ c/d e/f cf≡ed i) = record
+          { fst = lemma< a/b c/d e/f cf≡ed i
+          ; snd = isProp→PathP (λ i → isPropIsProp {A = lemma< a/b c/d e/f cf≡ed i}) ℤ.isProp< ℤ.isProp< i
+          }
+        fun₀ a/b (squash/ x y p q i j) = isSet→SquareP (λ _ _ → isSetHProp)
+          (λ _ → fun₀ a/b x)
+          (λ _ → fun₀ a/b y)
+          (λ i → fun₀ a/b (p i))
+          (λ i → fun₀ a/b (q i)) j i
+
+        toPath : ∀ a/b c/d (x : a/b ∼ c/d) (y : ℚ) → fun₀ a/b y ≡ fun₀ c/d y
+        toPath (a , b) (c , d) ad≡cb = elimProp (λ _ → isSetHProp _ _) λ (e , f) →
+          Σ≡Prop (λ _ → isPropIsProp) (ua (propBiimpl→Equiv ℤ.isProp< ℤ.isProp<
+                (ℤ.<-·o-cancel {k = -1+ b} ∘
+                  subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) ∙
+                                cong (ℤ._· ℕ₊₁→ℤ f) ad≡cb ∙
+                                ·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                               (·CommR e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∘
+                 ℤ.<-·o {k = -1+ d})
+                (ℤ.<-·o-cancel {k = -1+ d} ∘
+                  subst2 ℤ._<_ (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) ∙
+                                cong (ℤ._· ℕ₊₁→ℤ f) (sym ad≡cb) ∙
+                                ·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                               (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∘
+                 ℤ.<-·o {k = -1+ b})))
+
+        fun : ℚ → ℚ → hProp ℓ-zero
+        fun [ a/b ] y = fun₀ a/b y
+        fun (eq/ a/b c/d ad≡cb i) y = toPath a/b c/d ad≡cb y i
+        fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → isSetHProp)
+          (λ _ → fun x z) (λ _ → fun y z) (λ i → fun (p i) z) (λ i → fun (q i) z) j i
+
+_≤_ : ℚ → ℚ → Type₀
+m ≤ n = fst (m ≤' n)
+
+_<_ : ℚ → ℚ → Type₀
+m < n = fst (m <' n)
+
+_≥_ : ℚ → ℚ → Type₀
+m ≥ n = n ≤ m
+
+_>_ : ℚ → ℚ → Type₀
+m > n = n < m
+
+_#_ : ℚ → ℚ → Type₀
+m # n = (m < n) ⊎ (n < m)
+
+data Trichotomy (m n : ℚ) : Type₀ where
+  lt : m < n → Trichotomy m n
+  eq : m ≡ n → Trichotomy m n
+  gt : m > n → Trichotomy m n
+
+module _ where
+  open BinaryRelation
+
+  isProp≤ : isPropValued _≤_
+  isProp≤ m n = snd (m ≤' n)
+
+  isProp< : isPropValued _<_
+  isProp< m n = snd (m <' n)
+
+  isRefl≤ : isRefl _≤_
+  isRefl≤ = elimProp {P = λ x → x ≤ x} (λ x → isProp≤ x x) λ _ → ℤ.isRefl≤
+
+  isIrrefl< : isIrrefl _<_
+  isIrrefl< = elimProp {P = λ x → ¬ x < x} (λ _ → isProp¬ _) λ _ → ℤ.isIrrefl<
+
+  isAntisym≤ : isAntisym _≤_
+  isAntisym≤ =
+    elimProp2 {P = λ a b → a ≤ b → b ≤ a → a ≡ b}
+              (λ x y → isPropΠ2 λ _ _ → isSetℚ x y)
+              λ a b a≤b b≤a → eq/ a b (ℤ.isAntisym≤ a≤b b≤a)
+
+  isTrans≤ : isTrans _≤_
+  isTrans≤ =
+    elimProp3 {P = λ a b c → a ≤ b → b ≤ c → a ≤ c}
+              (λ x _ z → isPropΠ2 λ _ _ → isProp≤ x z)
+              λ { (a , b) (c , d) (e , f) ad≤cb cf≤ed →
+                ℤ.≤-·o-cancel {k = -1+ d}
+                  (subst (ℤ._≤ e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d)
+                    (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                  (ℤ.isTrans≤ (ℤ.≤-·o {k = ℕ₊₁→ℕ f} ad≤cb)
+                    (subst2 ℤ._≤_
+                      (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                      (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                      (ℤ.≤-·o {k = ℕ₊₁→ℕ b} cf≤ed)))) }
+
+  isTrans< : isTrans _<_
+  isTrans< =
+    elimProp3 {P = λ a b c → a < b → b < c → a < c}
+              (λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
+              λ { (a , b) (c , d) (e , f) ad<cb cf<ed →
+                ℤ.<-·o-cancel {k = -1+ d}
+                  (subst (ℤ._< e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d)
+                    (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                  (ℤ.isTrans< (ℤ.<-·o {k = -1+ f} ad<cb)
+                    (subst2 ℤ._<_
+                      (·CommR c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                      (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                      (ℤ.<-·o {k = -1+ b} cf<ed)))) }
+
+  isAsym< : isAsym _<_
+  isAsym< = isIrrefl×isTrans→isAsym _<_ (isIrrefl< , isTrans<)
+
+  isStronglyConnected≤ : isStronglyConnected _≤_
+  isStronglyConnected≤ =
+    elimProp2 {P = λ a b → (a ≤ b) ⊔′ (b ≤ a)}
+              (λ _ _ → isPropPropTrunc)
+               λ a b → ∣ lem a b ∣₁
+    where
+      lem : (a b : ℤ.ℤ × ℕ₊₁) → ([ a ] ≤ [ b ]) ⊎ ([ b ] ≤ [ a ])
+      lem (a , b) (c , d) with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
+      ... | ℤ.lt ad<cb = inl (ℤ.<-weaken ad<cb)
+      ... | ℤ.eq ad≡cb = inl (0 , ad≡cb)
+      ... | ℤ.gt cb<ad = inr (ℤ.<-weaken cb<ad)
+
+  isConnected< : isConnected _<_
+  isConnected< =
+    elimProp2 {P = λ a b → ¬ a ≡ b → (a < b) ⊔′ (b < a)}
+              (λ _ _ → isProp→ isPropPropTrunc)
+               λ a b ¬a≡b → ∣ lem a b ¬a≡b ∣₁
+    where
+      -- Agda can't infer the relation involved, so the signature looks a bit weird here
+      lem : (a b : ℤ.ℤ × ℕ₊₁) → ¬ [_] {R = _∼_} a ≡ [ b ] → ([ a ] < [ b ]) ⊎ ([ b ] < [ a ])
+      lem (a , b) (c , d) ¬a≡b with (a ℤ.· ℕ₊₁→ℤ d) ℤ.≟ (c ℤ.· ℕ₊₁→ℤ b)
+      ... | ℤ.lt ad<cb = inl ad<cb
+      ... | ℤ.eq ad≡cb = ⊥.rec (¬a≡b (eq/ (a , b) (c , d) ad≡cb))
+      ... | ℤ.gt cb<ad = inr cb<ad
+
+  isWeaklyLinear< : isWeaklyLinear _<_
+  isWeaklyLinear< =
+    elimProp3 {P = λ a b c → a < b → (a < c) ⊔′ (c < b)}
+              (λ _ _ _ → isProp→ isPropPropTrunc)
+               lem
+    where
+      lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] < [ b ] → ([ a ] < [ c ]) ⊔′ ([ c ] < [ b ])
+      lem a b c a<b with discreteℚ [ a ] [ c ]
+      ... | yes a≡c = ∣ inr (subst (_< [ b ]) a≡c a<b) ∣₁
+      ... | no a≢c = ∥₁.map (⊎.map (λ a<c → a<c)
+                                    (λ c<a → isTrans< [ c ] [ a ] [ b ] c<a a<b))
+                             (isConnected< [ a ] [ c ] a≢c)
+
+  isProp# : isPropValued _#_
+  isProp# x y = isProp⊎ (isProp< x y) (isProp< y x) (isAsym< x y)
+
+  isIrrefl# : isIrrefl _#_
+  isIrrefl# x (inl x<x) = isIrrefl< x x<x
+  isIrrefl# x (inr x<x) = isIrrefl< x x<x
+
+  isSym# : isSym _#_
+  isSym# _ _ (inl x<y) = inr x<y
+  isSym# _ _ (inr y<x) = inl y<x
+
+  isCotrans# : isCotrans _#_
+  isCotrans#
+    = elimProp3 {P = λ a b c → a # b → (a # c) ⊔′ (b # c)}
+                (λ _ _ _ → isProp→ isPropPropTrunc)
+                 lem
+      where
+        lem : (a b c : ℤ.ℤ × ℕ₊₁) → [ a ] # [ b ] → ([ a ] # [ c ]) ⊔′ ([ b ] # [ c ])
+        lem a b c a#b with discreteℚ [ b ] [ c ]
+        ... | yes b≡c = ∣ inl (subst ([ a ] #_) b≡c a#b) ∣₁
+        ... | no  b≢c = ∥₁.map inr (isConnected< [ b ] [ c ] b≢c)
+
+  inequalityImplies# : inequalityImplies _#_
+  inequalityImplies# a b = ∥₁.rec (isProp# a b) (λ a#b → a#b) ∘ (isConnected< a b)
+
+≤-+o : ∀ m n o → m ≤ n → m ℚ.+ o ≤ n ℚ.+ o
+≤-+o =
+  elimProp3 {P = λ a b c → a ≤ b → a ℚ.+ c ≤ b ℚ.+ c}
+            (λ x y z → isProp→ (isProp≤ (x ℚ.+ z) (y ℚ.+ z)))
+             λ { (a , b) (c , d) (e , f) ad≤cb →
+               subst2 ℤ._≤_
+                       (cong₂ ℤ._+_
+                              (cong (λ x → a ℤ.· ℕ₊₁→ℤ d ℤ.· x)
+                                    (ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
+                                    sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
+                                    cong (a ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
+                                    cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                                    sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))) ∙
+                                    ℤ.·Assoc a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f) ∙
+                                    cong (λ x → a ℤ.· ℕ₊₁→ℤ f ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
+                              (sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                                   cong (λ x → e ℤ.· ℕ₊₁→ℤ b ℤ.· x)
+                                        (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)))) ∙
+                              sym (ℤ.·DistL+ (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ (d ·₊₁ f))))
+                       (cong₂ ℤ._+_
+                              (cong (λ x → c ℤ.· ℕ₊₁→ℤ b ℤ.· x)
+                                    (ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
+                                    sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
+                                    cong (c ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
+                                    cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                                    sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))) ∙
+                                    ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f) ∙
+                                    cong (λ x → c ℤ.· ℕ₊₁→ℤ f ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
+                              (cong (ℤ._· ℕ₊₁→ℤ f)
+                                    (sym (ℤ.·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
+                                    cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
+                                    ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                    sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                                    cong (λ x → e ℤ.· ℕ₊₁→ℤ d ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)))) ∙
+                       sym (ℤ.·DistL+ (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ (b ·₊₁ f))))
+                       (ℤ.≤-+o {o = e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}
+                               (ℤ.≤-·o {k = ℕ₊₁→ℕ (f ·₊₁ f)} ad≤cb)) }
+
+≤-o+ : ∀ m n o →  m ≤ n → o ℚ.+ m ≤ o ℚ.+ n
+≤-o+ m n o = subst2 _≤_ (+Comm m o)
+                         (+Comm n o) ∘
+             ≤-+o m n o
+
+≤Monotone+ : ∀ m n o s → m ≤ n → o ≤ s → m ℚ.+ o ≤ n ℚ.+ s
+≤Monotone+ m n o s m≤n o≤s
+  = isTrans≤ (m ℚ.+ o)
+              (n ℚ.+ o)
+              (n ℚ.+ s)
+              (≤-+o m n o m≤n)
+              (≤-o+ o s n o≤s)
+
+≤-o+-cancel : ∀ m n o →  o ℚ.+ m ≤ o ℚ.+ n → m ≤ n
+≤-o+-cancel m n o
+  = subst2 _≤_ (+Assoc (- o) o m ∙ cong (ℚ._+ m) (+InvL o) ∙ +IdL m)
+                (+Assoc (- o) o n ∙ cong (ℚ._+ n) (+InvL o) ∙ +IdL n) ∘
+           ≤-o+ (o ℚ.+ m) (o ℚ.+ n) (- o)
+
+≤-+o-cancel : ∀ m n o → m ℚ.+ o ≤ n ℚ.+ o → m ≤ n
+≤-+o-cancel m n o
+  = subst2 _≤_ (sym (+Assoc m o (- o)) ∙ cong (λ x → m ℚ.+ x) (+InvR o) ∙ +IdR m)
+                (sym (+Assoc n o (- o)) ∙ cong (λ x → n ℚ.+ x) (+InvR o) ∙ +IdR n) ∘
+           ≤-+o (m ℚ.+ o) (n ℚ.+ o) (- o)
+
+<-+o : ∀ m n o → m < n → m ℚ.+ o < n ℚ.+ o
+<-+o =
+  elimProp3 {P = λ a b c → a < b → a ℚ.+ c < b ℚ.+ c}
+            (λ x y z → isProp→ (isProp< (x ℚ.+ z) (y ℚ.+ z)))
+             λ { (a , b) (c , d) (e , f) ad<cb →
+               subst2 ℤ._<_
+                       (cong₂ ℤ._+_
+                              (cong (λ x → a ℤ.· ℕ₊₁→ℤ d ℤ.· x)
+                                    (ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
+                                    sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
+                                    cong (a ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
+                                    cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                                    sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))) ∙
+                                    ℤ.·Assoc a (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f) ∙
+                                    cong (λ x → a ℤ.· ℕ₊₁→ℤ f ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
+                              (sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                                   cong (λ x → e ℤ.· ℕ₊₁→ℤ b ℤ.· x)
+                                        (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)))) ∙
+                       sym (ℤ.·DistL+ (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b) (ℕ₊₁→ℤ (d ·₊₁ f))))
+                       (cong₂ ℤ._+_
+                              (cong (λ x → c ℤ.· ℕ₊₁→ℤ b ℤ.· x)
+                                    (ℤ.pos·pos (ℕ₊₁→ℕ f) (ℕ₊₁→ℕ f)) ∙
+                                    sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ f)) ∙
+                                    cong (c ℤ.·_) (ℤ.·Assoc (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ f) ∙
+                                    cong (ℤ._· ℕ₊₁→ℤ f) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                                    sym (ℤ.·Assoc (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))) ∙
+                                    ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f) ∙
+                                    cong (λ x → c ℤ.· ℕ₊₁→ℤ f ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
+                              (cong (ℤ._· ℕ₊₁→ℤ f)
+                                    (sym (ℤ.·Assoc e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
+                                    cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
+                                    ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                    sym (ℤ.·Assoc (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                                    cong (λ x → e ℤ.· ℕ₊₁→ℤ d ℤ.· x)
+                                         (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)))) ∙
+                       sym (ℤ.·DistL+ (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ (b ·₊₁ f))))
+                       (ℤ.<-+o {o = e ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f}
+                               (ℤ.<-·o {k = -1+ (f ·₊₁ f)} ad<cb)) }
+
+<-o+ : ∀ m n o → m < n → o ℚ.+ m < o ℚ.+ n
+<-o+ m n o = subst2 _<_ (+Comm m o) (+Comm n o) ∘ <-+o m n o
+
+<Monotone+ : ∀ m n o s → m < n → o < s → m ℚ.+ o < n ℚ.+ s
+<Monotone+ m n o s m<n o<s
+  = isTrans< (m ℚ.+ o) (n ℚ.+ o) (n ℚ.+ s) (<-+o m n o m<n) (<-o+ o s n o<s)
+
+<-o+-cancel : ∀ m n o → o ℚ.+ m < o ℚ.+ n → m < n
+<-o+-cancel m n o
+  = subst2 _<_ (+Assoc (- o) o m ∙ cong (ℚ._+ m) (+InvL o) ∙ +IdL m)
+               (+Assoc (- o) o n ∙ cong (ℚ._+ n) (+InvL o) ∙ +IdL n) ∘
+           <-o+ (o ℚ.+ m) (o ℚ.+ n) (- o)
+
+<-+o-cancel : ∀ m n o → m ℚ.+ o < n ℚ.+ o → m < n
+<-+o-cancel m n o
+  = subst2 _<_ (sym (+Assoc m o (- o)) ∙ cong (λ x → m ℚ.+ x) (+InvR o) ∙ +IdR m)
+               (sym (+Assoc n o (- o)) ∙ cong (λ x → n ℚ.+ x) (+InvR o) ∙ +IdR n) ∘
+           <-+o (m ℚ.+ o) (n ℚ.+ o) (- o)
+
+<Weaken≤ : ∀ m n → m < n → m ≤ n
+<Weaken≤ m n = elimProp2 {P = λ x y → x < y → x ≤ y}
+                             (λ x y → isProp→ (isProp≤ x y))
+                             (λ { (a , b) (c , d) → ℤ.<-weaken }) m n
+
+isTrans<≤ : ∀ m n o → m < n → n ≤ o → m < o
+isTrans<≤ =
+    elimProp3 {P = λ a b c → a < b → b ≤ c → a < c}
+              (λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
+               λ { (a , b) (c , d) (e , f) ad<cb cf≤ed
+                → ℤ.<-·o-cancel {k = -1+ d}
+                 (ℤ.<≤-trans {m = c ℤ.· ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ b}
+                              (subst2 ℤ._<_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                                            (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                                            (ℤ.<-·o {k = -1+ f} ad<cb))
+                              (subst (_ ℤ.≤_) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                                     (ℤ.≤-·o {k = ℕ₊₁→ℕ b} cf≤ed)) )}
+
+isTrans≤< : ∀ m n o → m ≤ n → n < o → m < o
+isTrans≤< =
+    elimProp3 {P = λ a b c → a ≤ b → b < c → a < c}
+              (λ x _ z → isPropΠ2 λ _ _ → isProp< x z)
+               λ { (a , b) (c , d) (e , f) ad≤cb cf<ed
+                → ℤ.<-·o-cancel {k = -1+ d}
+                 (ℤ.≤<-trans {m = c ℤ.· ℕ₊₁→ℤ f ℤ.· ℕ₊₁→ℤ b}
+                              (subst2 ℤ._≤_ (·CommR a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+                                             (·CommR c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                                             (ℤ.≤-·o {k = ℕ₊₁→ℕ f} ad≤cb))
+                              (subst (_ ℤ.<_) (·CommR e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                                     (ℤ.<-·o {k = -1+ b} cf<ed)) )}
+
+≤-·o : ∀ m n o → 0 ≤ o → m ≤ n → m ℚ.· o ≤ n ℚ.· o
+≤-·o =
+  elimProp3 {P = λ a b c → 0 ≤ c → a ≤ b → a ℚ.· c ≤ b ℚ.· c}
+            (λ x y z → isPropΠ2 λ _ _ → isProp≤ (x ℚ.· z) (y ℚ.· z))
+             λ { (a , b) (c , d) (e , f) 0≤e ad≤cb
+             → subst2 ℤ._≤_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
+                              sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                              cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
+                             (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
+                              sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                              cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
+                             (ℤ.≤-·o {k = ℕ₊₁→ℕ f}
+                                      (ℤ.0≤o→≤-·o (subst (0 ℤ.≤_) (ℤ.·IdR e) 0≤e) ad≤cb)) }
+
+≤-·o-cancel : ∀ m n o → 0 < o → m ℚ.· o ≤ n ℚ.· o → m ≤ n
+≤-·o-cancel =
+  elimProp3 {P = λ a b c → 0 < c → a ℚ.· c ≤ b ℚ.· c → a ≤ b}
+            (λ x y _ → isPropΠ2 λ _ _ → isProp≤ x y)
+             λ { (a , b) (c , d) (e , f) 0<e aedf≤cebf
+             → ℤ.0<o→≤-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
+               (subst2 ℤ._≤_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
+                      (ℤ.≤-·o-cancel {k = -1+ f}
+                        (subst2 ℤ._≤_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
+                                       cong (λ x → a ℤ.· (e ℤ.· x))
+                                            (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
+                                             assoc {a} {e})
+                                       (sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
+                                        cong (λ x → c ℤ.· (e ℤ.· x))
+                                             (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
+                                              assoc {c} {e})
+                                        aedf≤cebf))) }
+
+  where assoc : ∀{a b c d} → a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
+        assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
+                                ℤ.·Assoc a (b ℤ.· c) d ∙
+                                cong (ℤ._· d) (ℤ.·Assoc a b c)
+
+<-·o : ∀ m n o → 0 < o → m < n → m ℚ.· o < n ℚ.· o
+<-·o =
+  elimProp3 {P = λ a b c → 0 < c → a < b → a ℚ.· c < b ℚ.· c}
+            (λ x y z → isPropΠ2 λ _ _ → isProp< (x ℚ.· z) (y ℚ.· z))
+             λ { (a , b) (c , d) (e , f) 0<e ad<cb
+             → subst2 ℤ._<_ (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR a (ℕ₊₁→ℤ d) e) ∙
+                             sym (ℤ.·Assoc (a ℤ.· e) (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f)) ∙
+                             cong (a ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))))
+                            (cong (ℤ._· ℕ₊₁→ℤ f) (·CommR c (ℕ₊₁→ℤ b) e) ∙
+                             sym (ℤ.·Assoc (c ℤ.· e) (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f)) ∙
+                             cong (c ℤ.· e ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))))
+                            (ℤ.<-·o {k = -1+ f}
+                                    (ℤ.0<o→<-·o (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e) ad<cb)) }
+
+<-·o-cancel : ∀ m n o → 0 < o → m ℚ.· o < n ℚ.· o → m < n
+<-·o-cancel =
+  elimProp3 {P = λ a b c → 0 < c → a ℚ.· c < b ℚ.· c → a < b}
+            (λ x y _ → isPropΠ2 λ _ _ → isProp< x y)
+             λ { (a , b) (c , d) (e , f) 0<e aedf<cebf
+             → ℤ.0<o→<-·o-cancel (subst (0 ℤ.<_) (ℤ.·IdR e) 0<e)
+               (subst2 ℤ._<_ (·CommR a e (ℕ₊₁→ℤ d)) (·CommR c e (ℕ₊₁→ℤ b))
+                      (ℤ.<-·o-cancel {k = -1+ f}
+                        (subst2 ℤ._<_ (sym (ℤ.·Assoc a e (ℕ₊₁→ℤ (d ·₊₁ f))) ∙
+                                       cong (λ x → a ℤ.· (e ℤ.· x))
+                                            (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f)) ∙
+                                             assoc {a} {e})
+                                       (sym (ℤ.·Assoc c e (ℕ₊₁→ℤ (b ·₊₁ f))) ∙
+                                        cong (λ x → c ℤ.· (e ℤ.· x))
+                                             (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f)) ∙
+                                              assoc {c} {e})
+                                        aedf<cebf))) }
+
+  where assoc : ∀{a b c d} → a ℤ.· (b ℤ.· (c ℤ.· d)) ≡ a ℤ.· b ℤ.· c ℤ.· d
+        assoc {a} {b} {c} {d} = cong (a ℤ.·_) (ℤ.·Assoc b c d) ∙
+                                ℤ.·Assoc a (b ℤ.· c) d ∙
+                                cong (ℤ._· d) (ℤ.·Assoc a b c)
+
+min≤ : ∀ m n → ℚ.min m n ≤ m
+min≤
+    = elimProp2 {P = λ a b → ℚ.min a b ≤ a}
+                (λ x y → isProp≤ (ℚ.min x y) x)
+                 λ { (a , b) (c , d)
+                  → subst2 ℤ._≤_ (sym (ℤ.·DistPosLMin (a ℤ.· ℕ₊₁→ℤ d)
+                                                       (c ℤ.· ℕ₊₁→ℤ b)
+                                                       (ℕ₊₁→ℕ b)))
+                                  (sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                   cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
+                                                  cong ℕ₊₁→ℤ (·₊₁-comm d b)))
+                                  (ℤ.min≤ {a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b}
+                                           {c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b}) }
+
+≤→min : ∀ m n → m ≤ n → ℚ.min m n ≡ m
+≤→min
+    = elimProp2 {P = λ a b → a ≤ b → ℚ.min a b ≡ a}
+                (λ x y → isProp→ (isSetℚ (ℚ.min x y) x))
+                 λ { (a , b) (c , d) ad≤cb
+                  → eq/ (ℤ.min (a ℤ.· ℕ₊₁→ℤ d)
+                               (c ℤ.· ℕ₊₁→ℤ b)
+                         , b ·₊₁ d)
+                        (a , b)
+                        (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.≤→min ad≤cb) ∙
+                         sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                         cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
+                                        cong ℕ₊₁→ℤ (·₊₁-comm d b))) }
+
+≤max : ∀ m n → m ≤ ℚ.max m n
+≤max
+    = elimProp2 {P = λ a b → a ≤ ℚ.max a b}
+                (λ x y → isProp≤ x (ℚ.max x y))
+                 λ { (a , b) (c , d)
+                  → subst2 ℤ._≤_ (sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                   cong (a ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
+                                                  cong ℕ₊₁→ℤ (·₊₁-comm d b)))
+                                  (sym (ℤ.·DistPosLMax (a ℤ.· ℕ₊₁→ℤ d)
+                                                       (c ℤ.· ℕ₊₁→ℤ b)
+                                                       (ℕ₊₁→ℕ b)))
+                                  (ℤ.≤max {a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b}
+                                           {c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b}) }
+
+≤→max : ∀ m n →  m ≤ n → ℚ.max m n ≡ n
+≤→max m n
+    = elimProp2 {P = λ a b → a ≤ b → ℚ.max a b ≡ b}
+                (λ x y → isProp→ (isSetℚ (ℚ.max x y) y))
+                (λ { (a , b) (c , d) ad≤cb
+                  → eq/ (ℤ.max (a ℤ.· ℕ₊₁→ℤ d)
+                               (c ℤ.· ℕ₊₁→ℤ b)
+                         , b ·₊₁ d)
+                        (c , d)
+                        (cong (ℤ._· ℕ₊₁→ℤ d) (ℤ.≤→max ad≤cb) ∙
+                         sym (ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d)) ∙
+                         cong (c ℤ.·_) (sym (ℤ.pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d)))) }) m n
+
+≤Dec : ∀ m n → Dec (m ≤ n)
+≤Dec = elimProp2 (λ x y → isPropDec (isProp≤ x y))
+       λ { (a , b) (c , d) → ℤ.≤Dec (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) }
+
+<Dec : ∀ m n → Dec (m < n)
+<Dec = elimProp2 (λ x y → isPropDec (isProp< x y))
+       λ { (a , b) (c , d) → ℤ.<Dec (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) }
+
+_≟_ : (m n : ℚ) → Trichotomy m n
+m ≟ n with discreteℚ m n
+... | yes m≡n = eq m≡n
+... | no m≢n with inequalityImplies# m n m≢n
+...             | inl m<n = lt m<n
+...             | inr n<m = gt n<m
+
+≤MonotoneMin : ∀ m n o s → m ≤ n → o ≤ s → ℚ.min m o ≤ ℚ.min n s
+≤MonotoneMin m n o s m≤n o≤s
+  = subst (_≤ ℚ.min n s)
+          (sym (ℚ.minAssoc n s (ℚ.min m o)) ∙
+           cong (ℚ.min n) (ℚ.minAssoc s m o ∙
+                           cong (λ a → ℚ.min a o) (ℚ.minComm s m) ∙
+                                 sym (ℚ.minAssoc m s o)) ∙
+                           ℚ.minAssoc n m (ℚ.min s o) ∙
+           cong₂ ℚ.min (ℚ.minComm n m ∙ ≤→min m n m≤n)
+                       (ℚ.minComm s o ∙ ≤→min o s o≤s))
+           (min≤ (ℚ.min n s) (ℚ.min m o))
+
+≤MonotoneMax : ∀ m n o s → m ≤ n → o ≤ s → ℚ.max m o ≤ ℚ.max n s
+≤MonotoneMax m n o s m≤n o≤s
+  = subst (ℚ.max m o ≤_)
+          (sym (ℚ.maxAssoc m o (ℚ.max n s)) ∙
+           cong (ℚ.max m) (ℚ.maxAssoc o n s ∙
+                           cong (λ a → ℚ.max a s) (ℚ.maxComm o n) ∙
+                                 sym (ℚ.maxAssoc n o s)) ∙
+                           ℚ.maxAssoc m n (ℚ.max o s) ∙
+           cong₂ ℚ.max (≤→max m n m≤n) (≤→max o s o≤s))
+          (≤max (ℚ.max m o) (ℚ.max n s))
+
+≡Weaken≤ : ∀ m n → m ≡ n → m ≤ n
+≡Weaken≤ m n m≡n = subst (m ≤_) m≡n (isRefl≤ m)
+
+≤→≯ : ∀ m n →  m ≤ n → ¬ (m > n)
+≤→≯ m n m≤n n<m = isIrrefl< n (subst (n <_) (isAntisym≤ m n m≤n (<Weaken≤ n m n<m)) n<m)
+
+≮→≥ : ∀ m n → ¬ (m < n) → m ≥ n
+≮→≥ m n m≮n with discreteℚ m n
+... | yes m≡n = ≡Weaken≤ n m (sym m≡n)
+... | no  m≢n = ∥₁.elim (λ _ → isProp≤ n m)
+                        (⊎.rec (⊥.rec ∘ m≮n) (<Weaken≤ n m))
+                        (isConnected< m n m≢n)
+
+0<+ : ∀ m n → 0 < m ℚ.+ n → (0 < m) ⊎ (0 < n)
+0<+ m n 0<m+n with <Dec 0 m | <Dec 0 n
+... | no 0≮m | no 0≮n = ⊥.rec (≤→≯ (m ℚ.+ n) 0 (≤Monotone+ m 0 n 0 (≮→≥ 0 m 0≮m) (≮→≥ 0 n 0≮n)) 0<m+n)
+... | no _    | yes 0<n = inr 0<n
+... | yes 0<m | _ = inl 0<m
diff --git a/Cubical/Data/Rationals/Properties.agda b/Cubical/Data/Rationals/Properties.agda
index 8adc74123c..100921a315 100644
--- a/Cubical/Data/Rationals/Properties.agda
+++ b/Cubical/Data/Rationals/Properties.agda
@@ -7,7 +7,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.GroupoidLaws hiding (_⁻¹)
 open import Cubical.Foundations.Univalence
 
-open import Cubical.Data.Int.MoreInts.QuoInt as ℤ using (ℤ; Sign; signed; pos; neg; posneg; sign)
+open import Cubical.Data.Int as ℤ using (ℤ; pos·pos; pos0+)
 open import Cubical.HITs.SetQuotients as SetQuotient using () renaming (_/_ to _//_)
 
 open import Cubical.Data.Nat as ℕ using (ℕ; zero; suc)
@@ -19,13 +19,19 @@ open import Cubical.Relation.Nullary
 
 open import Cubical.Data.Rationals.Base
 
-ℚ-cancelˡ : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.· a / c ·₊₁ b ] ≡ [ a / b ]
-ℚ-cancelˡ {a} {b} c = eq/ _ _
-  (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.·-comm (ℕ₊₁→ℤ c) a) ∙ sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))
+·CancelL : ∀ {a b} (c : ℕ₊₁) → [ ℕ₊₁→ℤ c ℤ.· a / c ·₊₁ b ] ≡ [ a / b ]
+·CancelL {a} {b} c = eq/ _ _
+  ((ℕ₊₁→ℤ c ℤ.· a)   ℤ.· ℕ₊₁→ℤ b  ≡⟨ cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.·Comm (ℕ₊₁→ℤ c) a) ⟩
+   (a ℤ.· (ℕ₊₁→ℤ c)) ℤ.· ℕ₊₁→ℤ b  ≡⟨ sym (ℤ.·Assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ⟩
+    a ℤ.· (ℕ₊₁→ℤ c   ℤ.· ℕ₊₁→ℤ b) ≡⟨ cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ c) (ℕ₊₁→ℕ b))) ⟩
+    a ℤ.·  ℕ₊₁→ℤ (c ·₊₁ b)         ∎)
 
-ℚ-cancelʳ : ∀ {a b} (c : ℕ₊₁) → [ a ℤ.· ℕ₊₁→ℤ c / b ·₊₁ c ] ≡ [ a / b ]
-ℚ-cancelʳ {a} {b} c = eq/ _ _
-  (sym (ℤ.·-assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ∙ cong (a ℤ.·_) (ℤ.·-comm (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)))
+·CancelR : ∀ {a b} (c : ℕ₊₁) → [ a ℤ.· ℕ₊₁→ℤ c / b ·₊₁ c ] ≡ [ a / b ]
+·CancelR {a} {b} c = eq/ _ _
+  (a ℤ.·  ℕ₊₁→ℤ c ℤ.· ℕ₊₁→ℤ b   ≡⟨ sym (ℤ.·Assoc a (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ⟩
+   a ℤ.· (ℕ₊₁→ℤ c ℤ.· ℕ₊₁→ℤ b)  ≡⟨ cong (a ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ c) (ℕ₊₁→ℤ b)) ⟩
+   a ℤ.· (ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ c)  ≡⟨ cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ c))) ⟩
+   a ℤ.· ℕ₊₁→ℤ (b ·₊₁ c) ∎)
 
 -- useful functions for defining operations on ℚ
 
@@ -40,11 +46,12 @@ onCommonDenom g g-eql g-eqr = SetQuotient.rec2 isSetℚ
   (λ { (a , b) (c , d) → [ g (a , b) (c , d) / b ·₊₁ d ] })
   (λ { (a , b) (c , d) (e , f) p → eql (a , b) (c , d) (e , f) p })
   (λ { (a , b) (c , d) (e , f) p → eqr (a , b) (c , d) (e , f) p })
-  where eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+  where abstract
+        eql : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
               → [ g (a , b) (e , f) / b ·₊₁ f ] ≡ [ g (c , d) (e , f) / d ·₊₁ f ]
         eql (a , b) (c , d) (e , f) p =
           [ g (a , b) (e , f) / b ·₊₁ f ]
-            ≡⟨ sym (ℚ-cancelˡ d) ⟩
+            ≡⟨ sym (·CancelL d) ⟩
           [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / d ·₊₁ (b ·₊₁ f) ]
             ≡[ i ]⟨ [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / ·₊₁-assoc d b f i ] ⟩
           [ ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) / (d ·₊₁ b) ·₊₁ f ]
@@ -52,13 +59,13 @@ onCommonDenom g g-eql g-eqr = SetQuotient.rec2 isSetℚ
           [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / (b ·₊₁ d) ·₊₁ f ]
             ≡[ i ]⟨ [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / ·₊₁-assoc b d f (~ i) ] ⟩
           [ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)) / b ·₊₁ (d ·₊₁ f) ]
-            ≡⟨ ℚ-cancelˡ b ⟩
+            ≡⟨ ·CancelL b ⟩
           [ g (c , d) (e , f) / d ·₊₁ f ] ∎
         eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
              → [ g (a , b) (c , d) / b ·₊₁ d ] ≡ [ g (a , b) (e , f) / b ·₊₁ f ]
         eqr (a , b) (c , d) (e , f) p =
           [ g (a , b) (c , d) / b ·₊₁ d ]
-            ≡⟨ sym (ℚ-cancelʳ f) ⟩
+            ≡⟨ sym (·CancelR f) ⟩
           [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / (b ·₊₁ d) ·₊₁ f ]
             ≡[ i ]⟨ [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / ·₊₁-assoc b d f (~ i) ] ⟩
           [ (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f / b ·₊₁ (d ·₊₁ f) ]
@@ -66,7 +73,7 @@ onCommonDenom g g-eql g-eqr = SetQuotient.rec2 isSetℚ
           [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / b ·₊₁ (f ·₊₁ d) ]
             ≡[ i ]⟨ [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / ·₊₁-assoc b f d i ] ⟩
           [ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d / (b ·₊₁ f) ·₊₁ d ]
-            ≡⟨ ℚ-cancelʳ d ⟩
+            ≡⟨ ·CancelR d ⟩
           [ g (a , b) (e , f) / b ·₊₁ f ] ∎
 
 onCommonDenomSym :
@@ -76,12 +83,13 @@ onCommonDenomSym :
            → ℕ₊₁→ℤ d ℤ.· (g (a , b) (e , f)) ≡ ℕ₊₁→ℤ b ℤ.· (g (c , d) (e , f)))
   → ℚ → ℚ → ℚ
 onCommonDenomSym g g-sym g-eql = onCommonDenom g g-eql q-eqr
-  where q-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
+  where abstract
+        q-eqr : ∀ ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : c ℤ.· ℕ₊₁→ℤ f ≡ e ℤ.· ℕ₊₁→ℤ d)
                 → (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡ (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d
         q-eqr (a , b) (c , d) (e , f) p =
-          (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡[ i ]⟨ ℤ.·-comm (g-sym (a , b) (c , d) i) (ℕ₊₁→ℤ f) i ⟩
+          (g (a , b) (c , d)) ℤ.· ℕ₊₁→ℤ f ≡[ i ]⟨ ℤ.·Comm (g-sym (a , b) (c , d) i) (ℕ₊₁→ℤ f) i ⟩
           ℕ₊₁→ℤ f ℤ.· (g (c , d) (a , b)) ≡⟨ g-eql (c , d) (e , f) (a , b) p ⟩
-          ℕ₊₁→ℤ d ℤ.· (g (e , f) (a , b)) ≡[ i ]⟨ ℤ.·-comm (ℕ₊₁→ℤ d) (g-sym (e , f) (a , b) i) i ⟩
+          ℕ₊₁→ℤ d ℤ.· (g (e , f) (a , b)) ≡[ i ]⟨ ℤ.·Comm (ℕ₊₁→ℤ d) (g-sym (e , f) (a , b) i) i ⟩
           (g (a , b) (e , f)) ℤ.· ℕ₊₁→ℤ d ∎
 
 onCommonDenomSym-comm : ∀ {g} g-sym {g-eql} (x y : ℚ)
@@ -96,96 +104,322 @@ onCommonDenomSym-comm g-sym = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
 infixl 6 _+_
 infixl 7 _·_
 
-private
+private abstract
   lem₁ : ∀ a b c d e (p : a ℤ.· b ≡ c ℤ.· d) → b ℤ.· (a ℤ.· e) ≡ d ℤ.· (c ℤ.· e)
-  lem₁ a b c d e p =   ℤ.·-assoc b a e
-                     ∙ cong (ℤ._· e) (ℤ.·-comm b a ∙ p ∙ ℤ.·-comm c d)
-                     ∙ sym (ℤ.·-assoc d c e)
+  lem₁ a b c d e p =   ℤ.·Assoc b a e
+                     ∙ cong (ℤ._· e) (ℤ.·Comm b a ∙ p ∙ ℤ.·Comm c d)
+                     ∙ sym (ℤ.·Assoc d c e)
 
   lem₂ : ∀ a b c → a ℤ.· (b ℤ.· c) ≡ c ℤ.· (b ℤ.· a)
-  lem₂ a b c =   cong (a ℤ.·_) (ℤ.·-comm b c) ∙ ℤ.·-assoc a c b
-               ∙ cong (ℤ._· b) (ℤ.·-comm a c) ∙ sym (ℤ.·-assoc c a b)
-               ∙ cong (c ℤ.·_) (ℤ.·-comm a b)
+  lem₂ a b c =   cong (a ℤ.·_) (ℤ.·Comm b c) ∙ ℤ.·Assoc a c b
+               ∙ cong (ℤ._· b) (ℤ.·Comm a c) ∙ sym (ℤ.·Assoc c a b)
+               ∙ cong (c ℤ.·_) (ℤ.·Comm a b)
+
+min : ℚ → ℚ → ℚ
+min = onCommonDenomSym
+  (λ { (a , b) (c , d) → ℤ.min (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+  (λ { (a , b) (c , d) → ℤ.minComm (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+   eq
+  where abstract
+    eq : ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+       → ℕ₊₁→ℤ d ℤ.· ℤ.min (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b)
+       ≡ ℕ₊₁→ℤ b ℤ.· ℤ.min (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d)
+    eq (a , b) (c , d) (e , f) p =
+      ℕ₊₁→ℤ d ℤ.· ℤ.min (a ℤ.· ℕ₊₁→ℤ f)
+                         (e ℤ.· ℕ₊₁→ℤ b)
+            ≡⟨ ℤ.·DistPosRMin (ℕ₊₁→ℕ d)
+                              (a ℤ.· ℕ₊₁→ℤ f)
+                              (e ℤ.· ℕ₊₁→ℤ b) ⟩
+      ℤ.min (ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f))
+            (ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b))
+            ≡⟨ cong₂ ℤ.min (ℤ.·Assoc (ℕ₊₁→ℤ d) a (ℕ₊₁→ℤ f))
+                           (ℤ.·Assoc (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b)) ⟩
+      ℤ.min (ℕ₊₁→ℤ d ℤ.· a ℤ.· ℕ₊₁→ℤ f)
+            (ℕ₊₁→ℤ d ℤ.· e ℤ.· ℕ₊₁→ℤ b)
+            ≡⟨ cong₂ ℤ.min (cong (ℤ._· ℕ₊₁→ℤ f)
+                                 (ℤ.·Comm (ℕ₊₁→ℤ d) a ∙
+                                  p ∙
+                                  ℤ.·Comm c (ℕ₊₁→ℤ b)) ∙
+                                  sym (ℤ.·Assoc (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ f)))
+                           (cong (ℤ._· ℕ₊₁→ℤ b)
+                                 (ℤ.·Comm (ℕ₊₁→ℤ d) e) ∙
+                                 ℤ.·Comm (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+      ℤ.min (ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f))
+            (ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d))
+            ≡⟨ sym (ℤ.·DistPosRMin (ℕ₊₁→ℕ b)
+                                   (c ℤ.· ℕ₊₁→ℤ f)
+                                   (e ℤ.· ℕ₊₁→ℤ d)) ⟩
+      ℕ₊₁→ℤ b ℤ.· ℤ.min (c ℤ.· ℕ₊₁→ℤ f)
+                         (e ℤ.· ℕ₊₁→ℤ d) ∎
+
+max : ℚ → ℚ → ℚ
+max = onCommonDenomSym
+  (λ { (a , b) (c , d) → ℤ.max (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+  (λ { (a , b) (c , d) → ℤ.maxComm (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+   eq
+  where abstract
+    eq : ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+       → ℕ₊₁→ℤ d ℤ.· ℤ.max (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b)
+       ≡ ℕ₊₁→ℤ b ℤ.· ℤ.max (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d)
+    eq (a , b) (c , d) (e , f) p =
+      ℕ₊₁→ℤ d ℤ.· ℤ.max (a ℤ.· ℕ₊₁→ℤ f)
+                         (e ℤ.· ℕ₊₁→ℤ b)
+            ≡⟨ ℤ.·DistPosRMax (ℕ₊₁→ℕ d)
+                              (a ℤ.· ℕ₊₁→ℤ f)
+                              (e ℤ.· ℕ₊₁→ℤ b) ⟩
+      ℤ.max (ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f))
+            (ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b))
+            ≡⟨ cong₂ ℤ.max (ℤ.·Assoc (ℕ₊₁→ℤ d) a (ℕ₊₁→ℤ f))
+                           (ℤ.·Assoc (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b)) ⟩
+      ℤ.max (ℕ₊₁→ℤ d ℤ.· a ℤ.· ℕ₊₁→ℤ f)
+            (ℕ₊₁→ℤ d ℤ.· e ℤ.· ℕ₊₁→ℤ b)
+            ≡⟨ cong₂ ℤ.max (cong (ℤ._· ℕ₊₁→ℤ f)
+                                 (ℤ.·Comm (ℕ₊₁→ℤ d) a ∙
+                                  p ∙
+                                  ℤ.·Comm c (ℕ₊₁→ℤ b)) ∙
+                                  sym (ℤ.·Assoc (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ f)))
+                           (cong (ℤ._· ℕ₊₁→ℤ b)
+                                 (ℤ.·Comm (ℕ₊₁→ℤ d) e) ∙
+                                 ℤ.·Comm (e ℤ.· ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ⟩
+      ℤ.max (ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f))
+            (ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d))
+            ≡⟨ sym (ℤ.·DistPosRMax (ℕ₊₁→ℕ b)
+                                   (c ℤ.· ℕ₊₁→ℤ f)
+                                   (e ℤ.· ℕ₊₁→ℤ d)) ⟩
+      ℕ₊₁→ℤ b ℤ.· ℤ.max (c ℤ.· ℕ₊₁→ℤ f)
+                         (e ℤ.· ℕ₊₁→ℤ d) ∎
+
+minComm : ∀ x y → min x y ≡ min y x
+minComm = onCommonDenomSym-comm
+  (λ { (a , b) (c , d) → ℤ.minComm (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+
+maxComm : ∀ x y → max x y ≡ max y x
+maxComm = onCommonDenomSym-comm
+  (λ { (a , b) (c , d) → ℤ.maxComm (a ℤ.· ℕ₊₁→ℤ d) (c ℤ.· ℕ₊₁→ℤ b) })
+
+minIdem : ∀ x → min x x ≡ x
+minIdem = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  λ { (a , b) → eq/ (ℤ.min (a ℤ.· ℕ₊₁→ℤ b) (a ℤ.· ℕ₊₁→ℤ b) , b ·₊₁ b) (a , b)
+                    (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.minIdem (a ℤ.· ℕ₊₁→ℤ b)) ∙
+                     sym (ℤ.·Assoc a (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ b)) ∙
+                     cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ b)))) }
+
+maxIdem : ∀ x → max x x ≡ x
+maxIdem = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  λ { (a , b) → eq/ (ℤ.max (a ℤ.· ℕ₊₁→ℤ b) (a ℤ.· ℕ₊₁→ℤ b) , b ·₊₁ b) (a , b)
+                    (cong (ℤ._· ℕ₊₁→ℤ b) (ℤ.maxIdem (a ℤ.· ℕ₊₁→ℤ b)) ∙
+                     sym (ℤ.·Assoc a (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ b)) ∙
+                     cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ b)))) }
+
+minAssoc : ∀ x y z → min x (min y z) ≡ min (min x y) z
+minAssoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  λ { (a , b) (c , d) (e , f) i
+    → [ (cong₂ ℤ.min
+               (cong (a ℤ.·_) (pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))
+               ∙ ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+               (ℤ.·DistPosLMin (c ℤ.· ℕ₊₁→ℤ f)
+                               (e ℤ.· ℕ₊₁→ℤ d)
+                               (ℕ₊₁→ℕ b)
+               ∙ cong₂ ℤ.min (sym (ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                             ∙ cong (c ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                             ∙ ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                             (sym (ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                             ∙ cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)
+                                             ∙ sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d)))))
+        ∙ ℤ.minAssoc (a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f)
+                     (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f)
+                     (e ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+        ∙ cong (λ x → ℤ.min x (e ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)))
+               (sym (ℤ.·DistPosLMin (a ℤ.· ℕ₊₁→ℤ d)
+                                    (c ℤ.· ℕ₊₁→ℤ b)
+                                    (ℕ₊₁→ℕ f)))) i / ·₊₁-assoc b d f i ] }
+
+maxAssoc : ∀ x y z → max x (max y z) ≡ max (max x y) z
+maxAssoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  λ { (a , b) (c , d) (e , f) i
+    → [ (cong₂ ℤ.max
+               (cong (a ℤ.·_) (pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))
+               ∙ ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ f))
+               (ℤ.·DistPosLMax (c ℤ.· ℕ₊₁→ℤ f)
+                               (e ℤ.· ℕ₊₁→ℤ d)
+                               (ℕ₊₁→ℕ b)
+               ∙ cong₂ ℤ.max (sym (ℤ.·Assoc c (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                             ∙ cong (c ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ f) (ℕ₊₁→ℤ b))
+                             ∙ ℤ.·Assoc c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))
+                             (sym (ℤ.·Assoc e (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b))
+                             ∙ cong (e ℤ.·_) (ℤ.·Comm (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)
+                                             ∙ sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d)))))
+        ∙ ℤ.maxAssoc (a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ f)
+                     (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ f)
+                     (e ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+        ∙ cong (λ x → ℤ.max x (e ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)))
+               (sym (ℤ.·DistPosLMax (a ℤ.· ℕ₊₁→ℤ d)
+                                    (c ℤ.· ℕ₊₁→ℤ b)
+                                    (ℕ₊₁→ℕ f)))) i / ·₊₁-assoc b d f i ] }
+
+minAbsorbLMax : ∀ x y → min x (max x y) ≡ x
+minAbsorbLMax = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
+  λ { (a , b) (c , d)
+    → eq/ (ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.max (a ℤ.· ℕ₊₁→ℤ d)
+                        (c ℤ.· ℕ₊₁→ℤ b)
+           ℤ.· ℕ₊₁→ℤ b) ,
+           b ·₊₁ (b ·₊₁ d))
+          (a , b)
+          (ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.max (a ℤ.· ℕ₊₁→ℤ d)
+                        (c ℤ.· ℕ₊₁→ℤ b)
+                         ℤ.· ℕ₊₁→ℤ b)
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (λ x → ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)) x
+                                  ℤ.· ℕ₊₁→ℤ b)
+                                (ℤ.·DistPosLMax (a ℤ.· ℕ₊₁→ℤ d) _ (ℕ₊₁→ℕ b)) ⟩
+           ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+          (ℤ.max (a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b)
+                 (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (λ x → ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                                (ℤ.max x (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+                                 ℤ.· ℕ₊₁→ℤ b)
+                                (sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                 cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
+                                                cong ℕ₊₁→ℤ (·₊₁-comm d b))) ⟩
+           ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+          (ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (ℤ._· ℕ₊₁→ℤ b)
+                                (ℤ.minAbsorbLMax (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)) _) ⟩
+           a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d) ℤ.· ℕ₊₁→ℤ b
+                 ≡⟨ sym (ℤ.·Assoc a (ℕ₊₁→ℤ (b ·₊₁ d)) (ℕ₊₁→ℤ b)) ∙
+                    cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ (b ·₊₁ d)) (ℕ₊₁→ℕ b)) ∙
+                                   cong ℕ₊₁→ℤ (·₊₁-comm (b ·₊₁ d) b)) ⟩
+           a ℤ.· ℕ₊₁→ℤ (b ·₊₁ (b ·₊₁ d)) ∎) }
+
+maxAbsorbLMin : ∀ x y → max x (min x y) ≡ x
+maxAbsorbLMin = SetQuotient.elimProp2 (λ _ _ → isSetℚ _ _)
+  λ { (a , b) (c , d)
+    → eq/ (ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.min (a ℤ.· ℕ₊₁→ℤ d)
+                        (c ℤ.· ℕ₊₁→ℤ b)
+                  ℤ.· ℕ₊₁→ℤ b) ,
+                  b ·₊₁ (b ·₊₁ d))
+                 (a , b)
+          (ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.min (a ℤ.· ℕ₊₁→ℤ d)
+                        (c ℤ.· ℕ₊₁→ℤ b)
+                  ℤ.· ℕ₊₁→ℤ b)
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (λ x → ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)) x
+                                  ℤ.· ℕ₊₁→ℤ b)
+                                (ℤ.·DistPosLMin (a ℤ.· ℕ₊₁→ℤ d) _ (ℕ₊₁→ℕ b)) ⟩
+           ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.min (a ℤ.· ℕ₊₁→ℤ d ℤ.· ℕ₊₁→ℤ b)
+                        (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (λ x → ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                                             (ℤ.min x (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+                                       ℤ.· ℕ₊₁→ℤ b)
+                                (sym (ℤ.·Assoc a (ℕ₊₁→ℤ d) (ℕ₊₁→ℤ b)) ∙
+                                 cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ b)) ∙
+                                                cong ℕ₊₁→ℤ (·₊₁-comm d b))) ⟩
+           ℤ.max (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                 (ℤ.min (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d))
+                        (c ℤ.· ℕ₊₁→ℤ b ℤ.· ℕ₊₁→ℤ b))
+           ℤ.· ℕ₊₁→ℤ b ≡⟨ cong (ℤ._· ℕ₊₁→ℤ b)
+                                (ℤ.maxAbsorbLMin (a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d)) _) ⟩
+           a ℤ.· ℕ₊₁→ℤ (b ·₊₁ d) ℤ.· ℕ₊₁→ℤ b
+             ≡⟨ sym (ℤ.·Assoc a (ℕ₊₁→ℤ (b ·₊₁ d)) (ℕ₊₁→ℤ b)) ∙
+                cong (a ℤ.·_) (sym (pos·pos (ℕ₊₁→ℕ (b ·₊₁ d)) (ℕ₊₁→ℕ b)) ∙
+                               cong ℕ₊₁→ℤ (·₊₁-comm (b ·₊₁ d) b)) ⟩
+           a ℤ.· ℕ₊₁→ℤ (b ·₊₁ (b ·₊₁ d)) ∎) }
 
 _+_ : ℚ → ℚ → ℚ
 _+_ = onCommonDenomSym
   (λ { (a , b) (c , d) → a ℤ.· (ℕ₊₁→ℤ d) ℤ.+ c ℤ.· (ℕ₊₁→ℤ b) })
-  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
-  (λ { (a , b) (c , d) (e , f) p →
-    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ b)
-      ≡⟨ sym (ℤ.·-distribˡ (ℕ₊₁→ℤ d) (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b)) ⟩
-    ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b)
-      ≡[ i ]⟨ lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) p i ℤ.+ lem₂ (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b) i ⟩
-    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d)
-      ≡⟨ ℤ.·-distribˡ (ℕ₊₁→ℤ b) (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) ⟩
-    ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ∎ })
-
-+-comm : ∀ x y → x + y ≡ y + x
-+-comm = onCommonDenomSym-comm
-  (λ { (a , b) (c , d) → ℤ.+-comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
-
-+-identityˡ : ∀ x → 0 + x ≡ x
-+-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
-  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityˡ b i ] })
-
-+-identityʳ : ∀ x → x + 0 ≡ x
-+-identityʳ x = +-comm x _ ∙ +-identityˡ x
-
-+-assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
-+-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
-  (λ { (a , b) (c , d) (e , f) i → [ eq a (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ f) i / ·₊₁-assoc b d f i ] })
+  (λ { (a , b) (c , d) → ℤ.+Comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
+   eq
+  where abstract
+    eq : ((a , b) (c , d) (e , f) : ℤ × ℕ₊₁) (p : a ℤ.· ℕ₊₁→ℤ d ≡ c ℤ.· ℕ₊₁→ℤ b)
+       → ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ b)
+       ≡ ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d)
+    eq (a , b) (c , d) (e , f) p =
+      ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ b)
+        ≡⟨ ℤ.·DistR+ (ℕ₊₁→ℤ d) (a ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ b) ⟩
+      ℕ₊₁→ℤ d ℤ.· (a ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ d ℤ.· (e ℤ.· ℕ₊₁→ℤ b)
+        ≡[ i ]⟨ lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) p i ℤ.+ lem₂ (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ b) i ⟩
+      ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ ℕ₊₁→ℤ b ℤ.· (e ℤ.· ℕ₊₁→ℤ d)
+        ≡⟨ sym (ℤ.·DistR+ (ℕ₊₁→ℤ b) (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d)) ⟩
+      ℕ₊₁→ℤ b ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ∎
+
++Comm : ∀ x y → x + y ≡ y + x
++Comm = onCommonDenomSym-comm
+  (λ { (a , b) (c , d) → ℤ.+Comm (a ℤ.· (ℕ₊₁→ℤ d)) (c ℤ.· (ℕ₊₁→ℤ b)) })
+
++IdL : ∀ x → 0 + x ≡ x
++IdL = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  λ { (a , b) i → [ ((cong (ℤ._+ a ℤ.· ℕ₊₁→ℤ 1) (ℤ.·AnnihilL (ℕ₊₁→ℤ b))
+                    ∙ sym (pos0+ (a ℤ.· ℕ₊₁→ℤ 1)))
+                    ∙ ℤ.·IdR a) i / ·₊₁-identityˡ b i ] }
+
++IdR : ∀ x → x + 0 ≡ x
++IdR x = +Comm x _ ∙ +IdL x
+
++Assoc : ∀ x y z → x + (y + z) ≡ (x + y) + z
++Assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) i
+    → [ (cong (λ x → a ℤ.· x ℤ.+ (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d) ℤ.· ℕ₊₁→ℤ b)
+              (pos·pos (ℕ₊₁→ℕ d) (ℕ₊₁→ℕ f))
+       ∙ eq a (ℕ₊₁→ℤ b) c (ℕ₊₁→ℤ d) e (ℕ₊₁→ℤ f)
+       ∙ cong (λ x → (a ℤ.· ℕ₊₁→ℤ d ℤ.+ c ℤ.· ℕ₊₁→ℤ b) ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· x)
+              (sym (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d)))) i / ·₊₁-assoc b d f i ] })
   where eq₁ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ a ℤ.· (c ℤ.· b)
-        eq₁ a b c = sym (ℤ.·-assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·-comm b c)
+        eq₁ a b c = sym (ℤ.·Assoc a b c) ∙ cong (a ℤ.·_) (ℤ.·Comm b c)
         eq₂ : ∀ a b c → (a ℤ.· b) ℤ.· c ≡ (a ℤ.· c) ℤ.· b
-        eq₂ a b c = eq₁ a b c ∙ ℤ.·-assoc a c b
+        eq₂ a b c = eq₁ a b c ∙ ℤ.·Assoc a c b
 
         eq : ∀ a b c d e f → Path ℤ _ _
         eq a b c d e f =
           a ℤ.· (d ℤ.· f) ℤ.+ (c ℤ.· f ℤ.+ e ℤ.· d) ℤ.· b
-            ≡[ i ]⟨ a ℤ.· (d ℤ.· f) ℤ.+ ℤ.·-distribʳ (c ℤ.· f) (e ℤ.· d) b (~ i) ⟩
+            ≡[ i ]⟨ a ℤ.· (d ℤ.· f) ℤ.+ ℤ.·DistL+ (c ℤ.· f) (e ℤ.· d) b i ⟩
           a ℤ.· (d ℤ.· f) ℤ.+ ((c ℤ.· f) ℤ.· b ℤ.+ (e ℤ.· d) ℤ.· b)
-            ≡[ i ]⟨ ℤ.+-assoc (ℤ.·-assoc a d f i) (eq₂ c f b i) (eq₁ e d b i) i ⟩
+            ≡[ i ]⟨ ℤ.+Assoc (ℤ.·Assoc a d f i) (eq₂ c f b i) (eq₁ e d b i) i ⟩
           ((a ℤ.· d) ℤ.· f ℤ.+ (c ℤ.· b) ℤ.· f) ℤ.+ e ℤ.· (b ℤ.· d)
-            ≡[ i ]⟨ ℤ.·-distribʳ (a ℤ.· d) (c ℤ.· b) f i ℤ.+ e ℤ.· (b ℤ.· d) ⟩
+            ≡[ i ]⟨ ℤ.·DistL+ (a ℤ.· d) (c ℤ.· b) f (~ i) ℤ.+ e ℤ.· (b ℤ.· d) ⟩
           (a ℤ.· d ℤ.+ c ℤ.· b) ℤ.· f ℤ.+ e ℤ.· (b ℤ.· d) ∎
 
 
 _·_ : ℚ → ℚ → ℚ
 _·_ = onCommonDenomSym
   (λ { (a , _) (c , _) → a ℤ.· c })
-  (λ { (a , _) (c , _) → ℤ.·-comm a c })
+  (λ { (a , _) (c , _) → ℤ.·Comm a c })
   (λ { (a , b) (c , d) (e , _) p → lem₁ a (ℕ₊₁→ℤ d) c (ℕ₊₁→ℤ b) e p })
 
-·-comm : ∀ x y → x · y ≡ y · x
-·-comm = onCommonDenomSym-comm (λ { (a , _) (c , _) → ℤ.·-comm a c })
+·Comm : ∀ x y → x · y ≡ y · x
+·Comm = onCommonDenomSym-comm (λ { (a , _) (c , _) → ℤ.·Comm a c })
 
-·-identityˡ : ∀ x → 1 · x ≡ x
-·-identityˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
-  (λ { (a , b) i → [ ℤ.·-identityˡ a i / ·₊₁-identityˡ b i ] })
+·IdL : ∀ x → 1 · x ≡ x
+·IdL = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) i → [ ℤ.·IdL a i / ·₊₁-identityˡ b i ] })
 
-·-identityʳ : ∀ x → x · 1 ≡ x
-·-identityʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
-  (λ { (a , b) i → [ ℤ.·-identityʳ a i / ·₊₁-identityʳ b i ] })
+·IdR : ∀ x → x · 1 ≡ x
+·IdR = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) i → [ ℤ.·IdR a i / ·₊₁-identityʳ b i ] })
 
-·-zeroˡ : ∀ x → 0 · x ≡ 0
-·-zeroˡ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
-  (λ { (a , b) → (λ i → [ p a b i / 1 ·₊₁ b ]) ∙ ℚ-cancelʳ b })
+·AnnihilL : ∀ x → 0 · x ≡ 0
+·AnnihilL = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) → (λ i → [ p a b i / 1 ·₊₁ b ]) ∙ ·CancelR b })
   where p : ∀ a b → 0 ℤ.· a ≡ 0 ℤ.· ℕ₊₁→ℤ b
-        p a b = ℤ.·-zeroˡ {ℤ.spos} a ∙ sym (ℤ.·-zeroˡ {ℤ.spos} (ℕ₊₁→ℤ b))
+        p a b = ℤ.·AnnihilL a ∙ sym (ℤ.·AnnihilL (ℕ₊₁→ℤ b))
 
-·-zeroʳ : ∀ x → x · 0 ≡ 0
-·-zeroʳ = SetQuotient.elimProp (λ _ → isSetℚ _ _)
-  (λ { (a , b) → (λ i → [ p a b i / b ·₊₁ 1 ]) ∙ ℚ-cancelˡ b })
+·AnnihilR : ∀ x → x · 0 ≡ 0
+·AnnihilR = SetQuotient.elimProp (λ _ → isSetℚ _ _)
+  (λ { (a , b) → (λ i → [ p a b i / b ·₊₁ 1 ]) ∙ ·CancelL b })
   where p : ∀ a b → a ℤ.· 0 ≡ ℕ₊₁→ℤ b ℤ.· 0
-        p a b = ℤ.·-zeroʳ {ℤ.spos} a ∙ sym (ℤ.·-zeroʳ {ℤ.spos} (ℕ₊₁→ℤ b))
+        p a b = ℤ.·AnnihilR a ∙ sym (ℤ.·AnnihilR (ℕ₊₁→ℤ b))
 
-·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
-·-assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
-  (λ { (a , b) (c , d) (e , f) i → [ ℤ.·-assoc a c e i / ·₊₁-assoc b d f i ] })
+·Assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z
+·Assoc = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) i → [ ℤ.·Assoc a c e i / ·₊₁-assoc b d f i ] })
 
-·-distribˡ : ∀ x y z → (x · y) + (x · z) ≡ x · (y + z)
-·-distribˡ = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
-  (λ { (a , b) (c , d) (e , f) → eq a b c d e f })
+·DistL+ : ∀ x y z → x · (y + z) ≡ (x · y) + (x · z)
+·DistL+ = SetQuotient.elimProp3 (λ _ _ _ → isSetℚ _ _)
+  (λ { (a , b) (c , d) (e , f) → sym (eq a b c d e f)})
   where lem : ∀ {ℓ} {A : Type ℓ} (_·_ : A → A → A)
                 (·-comm : ∀ x y → x · y ≡ y · x)
                 (·-assoc : ∀ x y z → x · (y · z) ≡ (x · y) · z)
@@ -197,7 +431,7 @@ _·_ = onCommonDenomSym
           ((a · c) · d) · b ≡[ i ]⟨ ·-assoc a c d (~ i) · b ⟩
           (a · (c · d)) · b ∎
 
-        lemℤ   = lem ℤ._·_ ℤ.·-comm ℤ.·-assoc
+        lemℤ   = lem ℤ._·_ ℤ.·Comm ℤ.·Assoc
         lemℕ₊₁ = lem _·₊₁_ ·₊₁-comm ·₊₁-assoc
 
         eq : ∀ a b c d e f →
@@ -206,43 +440,47 @@ _·_ = onCommonDenomSym
              ≡ [ a ℤ.· (c ℤ.· ℕ₊₁→ℤ f ℤ.+ e ℤ.· ℕ₊₁→ℤ d)
                 / b ·₊₁ (d ·₊₁ f) ]
         eq a b c d e f =
-          (λ i → [ lemℤ a c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f) i ℤ.+ lemℤ a e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d) i
+          (λ i → [ (cong (a ℤ.· c ℤ.·_) (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ f))
+                 ∙ (lemℤ a c (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ f))) i
+                   ℤ.+
+                   (cong (a ℤ.· e ℤ.·_) (pos·pos (ℕ₊₁→ℕ b) (ℕ₊₁→ℕ d))
+                 ∙ (lemℤ a e (ℕ₊₁→ℤ b) (ℕ₊₁→ℤ d))) i
                    / lemℕ₊₁ b d b f i ]) ∙
-          (λ i → [ ℤ.·-distribʳ (a ℤ.· (c ℤ.· ℕ₊₁→ℤ f)) (a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)) (ℕ₊₁→ℤ b) i
+          (λ i → [ (sym (ℤ.·DistL+ (a ℤ.· (c ℤ.· ℕ₊₁→ℤ f)) (a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)) (ℕ₊₁→ℤ b))) i
                    / (b ·₊₁ (d ·₊₁ f)) ·₊₁ b ]) ∙
-          ℚ-cancelʳ {a ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)} {b ·₊₁ (d ·₊₁ f)} b ∙
-          (λ i → [ ℤ.·-distribˡ a (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d) i
+          ·CancelR {a ℤ.· (c ℤ.· ℕ₊₁→ℤ f) ℤ.+ a ℤ.· (e ℤ.· ℕ₊₁→ℤ d)} {b ·₊₁ (d ·₊₁ f)} b ∙
+          (λ i → [ (sym (ℤ.·DistR+ a (c ℤ.· ℕ₊₁→ℤ f) (e ℤ.· ℕ₊₁→ℤ d))) i
                    / b ·₊₁ (d ·₊₁ f) ])
 
-·-distribʳ : ∀ x y z → (x · z) + (y · z) ≡ (x + y) · z
-·-distribʳ x y z = (λ i → ·-comm x z i + ·-comm y z i) ∙ ·-distribˡ z x y ∙ ·-comm z (x + y)
+·DistR+ : ∀ x y z → (x + y) · z ≡ (x · z) + (y · z)
+·DistR+ x y z = sym ((λ i → ·Comm x z i + ·Comm y z i) ∙ (sym (·DistL+ z x y)) ∙ ·Comm z (x + y))
 
 
 -_ : ℚ → ℚ
 - x = -1 · x
 
-negate-invol : ∀ x → - - x ≡ x
-negate-invol x = ·-assoc -1 -1 x ∙ ·-identityˡ x
+-Invol : ∀ x → - - x ≡ x
+-Invol x = ·Assoc -1 -1 x ∙ ·IdL x
 
 negateEquiv : ℚ ≃ ℚ
-negateEquiv = isoToEquiv (iso -_ -_ negate-invol negate-invol)
+negateEquiv = isoToEquiv (iso -_ -_ -Invol -Invol)
 
 negateEq : ℚ ≡ ℚ
 negateEq = ua negateEquiv
 
-+-inverseˡ : ∀ x → (- x) + x ≡ 0
-+-inverseˡ x = (λ i → (-1 · x) + ·-identityˡ x (~ i)) ∙ ·-distribʳ -1 1 x ∙ ·-zeroˡ x
++InvL : ∀ x → (- x) + x ≡ 0
++InvL x = (λ i → (-1 · x) + ·IdL x (~ i)) ∙ (sym (·DistR+ -1 1 x)) ∙ ·AnnihilL x
 
 _-_ : ℚ → ℚ → ℚ
 x - y = x + (- y)
 
-+-inverseʳ : ∀ x → x - x ≡ 0
-+-inverseʳ x = +-comm x (- x) ∙ +-inverseˡ x
++InvR : ∀ x → x - x ≡ 0
++InvR x = +Comm x (- x) ∙ +InvL x
 
-+-injˡ : ∀ x y z → x + y ≡ x + z → y ≡ z
-+-injˡ x y z p = sym (q y) ∙ cong ((- x) +_) p ∙ q z
++CancelL : ∀ x y z → x + y ≡ x + z → y ≡ z
++CancelL x y z p = sym (q y) ∙ cong ((- x) +_) p ∙ q z
   where q : ∀ y → (- x) + (x + y) ≡ y
-        q y = +-assoc (- x) x y ∙ cong (_+ y) (+-inverseˡ x) ∙ +-identityˡ y
+        q y = +Assoc (- x) x y ∙ cong (_+ y) (+InvL x) ∙ +IdL y
 
-+-injʳ : ∀ x y z → x + y ≡ z + y → x ≡ z
-+-injʳ x y z p = +-injˡ y x z (+-comm y x ∙ p ∙ +-comm z y)
++CancelR : ∀ x y z → x + y ≡ z + y → x ≡ z
++CancelR x y z p = +CancelL y x z (+Comm y x ∙ p ∙ +Comm z y)
diff --git a/Cubical/HITs/SetQuotients/Properties.agda b/Cubical/HITs/SetQuotients/Properties.agda
index 372e64092e..02ca17a0f3 100644
--- a/Cubical/HITs/SetQuotients/Properties.agda
+++ b/Cubical/HITs/SetQuotients/Properties.agda
@@ -119,14 +119,32 @@ rec set f feq (squash/ x y p q i j) = set (g x) (g y) (cong g p) (cong g q) i j
   g = rec set f feq
 
 rec2 : isSet C
-  → (f : A → B → C)
-  → (∀ a b c → R a b → f a c ≡ f b c)
-  → (∀ a b c → S b c → f a b ≡ f a c)
-  → A / R → B / S → C
-rec2 set f feql feqr =
-  rec (isSetΠ (λ _ → set))
-    (λ a → rec set (f a) (feqr a))
-    (λ a b r → funExt (elimProp (λ _ → set _ _) (λ c → feql a b c r)))
+     → (f : A → B → C)
+     → (∀ a b c → R a b → f a c ≡ f b c)
+     → (∀ a b c → S b c → f a b ≡ f a c)
+     → A / R → B / S → C
+rec2 {_} {C} {_} {A} {_} {B} {_} {R} {_} {S} set f feql feqr = fun
+  where
+    fun₀ : A → B / S → C
+    fun₀ a [ b ] = f a b
+    fun₀ a (eq/ b c r i) = feqr a b c r i
+    fun₀ a (squash/ x y p q i j) = isSet→SquareP (λ _ _ → set)
+      (λ _ → fun₀ a x)
+      (λ _ → fun₀ a y)
+      (λ i → fun₀ a (p i))
+      (λ i → fun₀ a (q i)) j i
+
+    toPath : ∀ (a b : A) (x : R a b) (y : B / S) → fun₀ a y ≡ fun₀ b y
+    toPath a b rab = elimProp (λ _ → set _ _) λ c → feql a b c rab
+
+    fun : A / R → B / S → C
+    fun [ a ] y = fun₀ a y
+    fun (eq/ a b r i) y = toPath a b r y i
+    fun (squash/ x y p q i j) z = isSet→SquareP (λ _ _ → set)
+      (λ _ → fun x z)
+      (λ _ → fun y z)
+      (λ i → fun (p i) z)
+      (λ i → fun (q i) z) j i
 
 -- the recursor for maps into groupoids:
 -- i.e. for any type A with a binary relation R and groupoid B,
diff --git a/Cubical/Relation/Binary/Base.agda b/Cubical/Relation/Binary/Base.agda
index 68bb8f5d55..2f78c4dbf5 100644
--- a/Cubical/Relation/Binary/Base.agda
+++ b/Cubical/Relation/Binary/Base.agda
@@ -149,6 +149,9 @@ module BinaryRelation {ℓ ℓ' : Level} {A : Type ℓ} (R : Rel A A ℓ') where
   impliesIdentity : Type _
   impliesIdentity = {a a' : A} → (R a a') → (a ≡ a')
 
+  inequalityImplies : Type _
+  inequalityImplies = (a b : A) → ¬ a ≡ b → R a b
+
   -- the total space corresponding to the binary relation w.r.t. a
   relSinglAt : (a : A) → Type (ℓ-max ℓ ℓ')
   relSinglAt a = Σ[ a' ∈ A ] (R a a')
diff --git a/Cubical/Tactics/CommRingSolver/RawAlgebra.agda b/Cubical/Tactics/CommRingSolver/RawAlgebra.agda
index 7cfef8b8d6..15147f1658 100644
--- a/Cubical/Tactics/CommRingSolver/RawAlgebra.agda
+++ b/Cubical/Tactics/CommRingSolver/RawAlgebra.agda
@@ -14,6 +14,9 @@ open import Cubical.Data.Int
   ; -DistL· to -ℤDistL·ℤ
   ; ·DistR+ to ·ℤDistR+
   ; ·DistL+ to ·ℤDistL+)
+  hiding
+  ( ·IdL
+  ; ·IdR)
 
 open import Cubical.Tactics.CommRingSolver.RawRing renaming (⟨_⟩ to ⟨_⟩ᵣ)
 open import Cubical.Tactics.CommRingSolver.IntAsRawRing