From 52aaeade9fd9fb9af90c2f7742ec93c73e580861 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 10 Feb 2025 08:41:57 +0000
Subject: [PATCH 01/25] refactor: use the definitions!

---
 src/Relation/Binary/Definitions.agda | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 167b63a8cb..c8c4ba1ecd 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -155,19 +155,19 @@ Monotonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
 Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_
 
 Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
-Antitonic₁ _≤_ _⊑_ f = f Preserves (flip _≤_) ⟶ _⊑_
+Antitonic₁ _≤_ = Monotonic₁ (flip _≤_)
 
 Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
 Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_
 
 MonotonicAntitonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
-MonotonicAntitonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ (flip _⊑_) ⟶ _≼_
+MonotonicAntitonic _≤_ _⊑_ = Monotonic₂ _≤_ (flip _⊑_)
 
 AntitonicMonotonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
-AntitonicMonotonic _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ _⊑_ ⟶ _≼_
+AntitonicMonotonic _≤_ = Monotonic₂ (flip _≤_)
 
 Antitonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
-Antitonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ (flip _≤_) ⟶ (flip _⊑_) ⟶ _≼_
+Antitonic₂ _≤_ _⊑_ = Monotonic₂ (flip _≤_) (flip _⊑_)
 
 Adjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
 Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)

From e19936cb21024ad14059a3387cc592e5c98fe591 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 13 Feb 2025 22:25:02 +0000
Subject: [PATCH 02/25] add: `LeftMonotonic` and `RightMonotonic`

---
 CHANGELOG.md                          | 16 ++++++++++++++++
 src/Algebra/Definitions.agda          |  4 ++--
 src/Relation/Binary/Consequences.agda | 26 ++++++++++++++++++++------
 src/Relation/Binary/Definitions.agda  |  6 ++++++
 4 files changed, 44 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 51ce0b89dd..a99bafe7b7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -108,3 +108,19 @@ Additions to existing modules
   quasiring                       : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ)
   commutativeRing                 : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ)
   ```
+
+* In `Relation.Binary.Consequences`:
+  ```agda
+  mono₂⇒monoˡ : Reflexive ≤₁ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
+  mono₂⇒monoˡ : Reflexive ≤₂ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
+  monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ →
+                      LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
+                      Monotonic₂ ≤₁ ≤₂ ≤₃ f
+  ```
+
+* In `Relation.Binary.Definitions`:
+  ```agda
+  LeftMonotonic  : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+  RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+  ```
+
diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index 62528e5b70..b823ee3e58 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -37,10 +37,10 @@ Congruent₂ : Op₂ A → Set _
 Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
 
 LeftCongruent : Op₂ A → Set _
-LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
+LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)
 
 RightCongruent : Op₂ A → Set _
-RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
+RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x)
 
 Associative : Op₂ A → Set _
 Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 3cdb4db356..bfa8a782a5 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -23,7 +23,7 @@ open import Relation.Unary using (∁; Pred)
 private
   variable
     a ℓ ℓ₁ ℓ₂ ℓ₃ ℓ₄ p : Level
-    A B : Set a
+    A B C : Set a
 
 ------------------------------------------------------------------------
 -- Substitutive properties
@@ -87,24 +87,38 @@ module _ {_≈_ : Rel A ℓ₁} {_≤_ : Rel A ℓ₂} where
 module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃} {≤₂ : Rel B ℓ₄} where
 
   mono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
-              ∀ {f} → f Preserves ≤₁ ⟶ ≤₂ → f Preserves ≈₁ ⟶ ≈₂
+              ∀ {f} → Monotonic₁ ≤₁ ≤₂ f → Monotonic₁ ≈₁ ≈₂ f
   mono⇒cong sym reflexive antisym mono x≈y = antisym
     (mono (reflexive x≈y))
     (mono (reflexive (sym x≈y)))
 
   antimono⇒cong : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
-                  ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → f Preserves ≈₁ ⟶ ≈₂
+                  ∀ {f} → f Preserves ≤₁ ⟶ (flip ≤₂) → Monotonic₁ ≈₁ ≈₂ f
   antimono⇒cong sym reflexive antisym antimono p≈q = antisym
     (antimono (reflexive (sym p≈q)))
     (antimono (reflexive p≈q))
 
-  mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ → ∀ {f} →
-                f Preserves₂ ≤₁ ⟶ ≤₁ ⟶ ≤₂ →
-                f Preserves₂ ≈₁ ⟶ ≈₁ ⟶ ≈₂
+  mono₂⇒cong₂ : Symmetric ≈₁ → ≈₁ ⇒ ≤₁ → Antisymmetric ≈₂ ≤₂ →
+                ∀ {f} → Monotonic₂ ≤₁ ≤₁ ≤₂ f → Monotonic₂ ≈₁ ≈₁ ≈₂ f
   mono₂⇒cong₂ sym reflexive antisym mono x≈y u≈v = antisym
     (mono (reflexive x≈y) (reflexive u≈v))
     (mono (reflexive (sym x≈y)) (reflexive (sym u≈v)))
 
+module _ {≤₁ : Rel A ℓ₁} {≤₂ : Rel B ℓ₂} {≤₃ : Rel C ℓ₂} where
+
+  mono₂⇒monoˡ : Reflexive ≤₁ →
+                ∀ {f} → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
+  mono₂⇒monoˡ refl mono = mono refl
+
+  mono₂⇒monoʳ : Reflexive ≤₂ →
+                ∀ {f} → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
+  mono₂⇒monoʳ refl mono = flip mono refl
+
+  monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ →
+                      ∀ {f} → LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
+                      Monotonic₂ ≤₁ ≤₂ ≤₃ f
+  monoˡ∧monoʳ⇒mono₂ trans monoˡ monoʳ x≤₁y u≤₂v = trans (monoˡ u≤₂v) (monoʳ x≤₁y)
+
 ------------------------------------------------------------------------
 -- Proofs for strict orders
 
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index c8c4ba1ecd..95ed9a18ac 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -157,6 +157,12 @@ Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_
 Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
 Antitonic₁ _≤_ = Monotonic₁ (flip _≤_)
 
+LeftMonotonic : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+LeftMonotonic _≤_ _⊑_ _∙_ = ∀ {x} → Monotonic₁ _≤_ _⊑_ (x ∙_)
+
+RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+RightMonotonic _≤_ _⊑_ _∙_ = ∀ {y} → Monotonic₁ _≤_ _⊑_ (_∙ y)
+
 Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
 Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_
 

From 3ac9569350170540597553710b00db5302b9b8b5 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 13 Feb 2025 23:14:47 +0000
Subject: [PATCH 03/25] refactor: systematise `Congruence` reasoning

---
 src/Algebra/Consequences/Base.agda   | 14 ++++-
 src/Algebra/Consequences/Setoid.agda | 88 +++++++++++++++++-----------
 2 files changed, 67 insertions(+), 35 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 574ad48a16..048302f597 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -14,13 +14,23 @@ open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
 open import Relation.Binary.Core
+open import Relation.Binary.Consequences
+  using (mono₂⇒monoˡ; mono₂⇒monoʳ)
 open import Relation.Binary.Definitions using (Reflexive)
 
-module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
+module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
-  sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
+  sel⇒idem : Selective _≈_ _∙_ → Idempotent _≈_ _∙_
   sel⇒idem sel x = reduce (sel x x)
 
+  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
+
+    congˡ : LeftCongruent _≈_ _∙_
+    congˡ = mono₂⇒monoˡ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong
+
+    congʳ : RightCongruent _≈_ _∙_
+    congʳ = mono₂⇒monoʳ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong
+
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 66e441a9e0..9b90eba41a 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -14,46 +14,58 @@ open import Relation.Binary.Definitions
 
 module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open Setoid S renaming (Carrier to A)
 open import Algebra.Core
-open import Algebra.Definitions _≈_
+import Algebra.Consequences.Base as Base
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Consequences as Bin
-open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
 
+open Setoid S renaming (Carrier to A)
+open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid S
+
 ------------------------------------------------------------------------
 -- Re-exports
 
 -- Export base lemmas that don't require the setoid
 
-open import Algebra.Consequences.Base public
+open Base public
+  hiding (module Congruence)
+
+-- Export congruence lemmas using reflexivity
+
+module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
+
+  open Base.Congruence _≈_ cong refl public
+    renaming (congˡ to ∙-congˡ; congʳ to ∙-congʳ)
 
 ------------------------------------------------------------------------
 -- MiddleFourExchange
 
 module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 
+  open Congruence cong
+
   comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                           _∙_ MiddleFourExchange _∙_
   comm∧assoc⇒middleFour comm assoc w x y z = begin
     (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩
-    w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩
-    w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩
-    w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
-    w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
+    w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (assoc x y z) ⟨
+    w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
+    w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
+    w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
     (w ∙ y) ∙ (x ∙ z) ∎
 
   identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                               _∙_ MiddleFourExchange _∙_ →
                               Associative _∙_
   identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
-    (x ∙ y) ∙ z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+    (x ∙ y) ∙ z       ≈⟨ ∙-congˡ (identityˡ z) ⟨
     (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
-    (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
+    (x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩
     x ∙ (y ∙ z)       ∎
 
   identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
@@ -61,7 +73,7 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
                              Commutative _∙_
   identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
     = begin
-    x ∙ y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    x ∙ y             ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
     (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
     (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
     y ∙ x             ∎
@@ -198,14 +210,16 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
 
 module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
 
+  open Congruence cong
+
   assoc∧id∧invʳ⇒invˡ-unique : Associative _∙_ →
                               Identity e _∙_ → RightInverse e _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≈ e → x ≈ (y ⁻¹)
   assoc∧id∧invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin
-    x                ≈⟨ sym (idʳ x) ⟩
-    x ∙ e            ≈⟨ cong refl (sym (invʳ y)) ⟩
-    x ∙ (y ∙ (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩
-    (x ∙ y) ∙ (y ⁻¹) ≈⟨ cong eq refl ⟩
+    x                ≈⟨ idʳ x ⟨
+    x ∙ e            ≈⟨ ∙-congˡ (invʳ y) ⟨
+    x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
+    (x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩
     e ∙ (y ⁻¹)       ≈⟨ idˡ (y ⁻¹) ⟩
     y ⁻¹             ∎
 
@@ -213,10 +227,10 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh
                               Identity e _∙_ → LeftInverse e _⁻¹ _∙_ →
                               ∀ x y → (x ∙ y) ≈ e → y ≈ (x ⁻¹)
   assoc∧id∧invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin
-    y                ≈⟨ sym (idˡ y) ⟩
-    e ∙ y            ≈⟨ cong (sym (invˡ x)) refl ⟩
+    y                ≈⟨ idˡ y ⟨
+    e ∙ y            ≈⟨ ∙-congʳ (invˡ x) ⟨
     ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
-    (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
+    (x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
     (x ⁻¹) ∙ e       ≈⟨ idʳ (x ⁻¹) ⟩
     x ⁻¹             ∎
 
@@ -228,6 +242,8 @@ module _ {_∙_ _◦_ : Op₂ A}
          (∙-comm : Commutative _∙_)
          where
 
+  open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ)
+
   comm∧distrˡ⇒distrʳ :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
   comm∧distrˡ⇒distrʳ distrˡ x y z = begin
     (y ◦ z) ∙ x       ≈⟨ ∙-comm (y ◦ z) x ⟩
@@ -250,7 +266,7 @@ module _ {_∙_ _◦_ : Op₂ A}
 
   comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z)))
   comm⇒sym[distribˡ] x {y} {z} prf = begin
-    x ◦ (z ∙ y)       ≈⟨ ◦-cong refl (∙-comm z y) ⟩
+    x ◦ (z ∙ y)       ≈⟨ ◦-congˡ (∙-comm z y) ⟩
     x ◦ (y ∙ z)       ≈⟨ prf ⟩
     (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
     (x ◦ z) ∙ (x ◦ y) ∎
@@ -262,16 +278,18 @@ module _ {_∙_ _◦_ : Op₂ A}
          (◦-comm  : Commutative _◦_)
          where
 
+  open Congruence ∙-cong
+
   distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
                              _◦_ Absorbs _∙_ →
                              _◦_ DistributesOver _∙_ →
                              _∙_ DistributesOverˡ _◦_
   distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin
-    x ∙ (y ◦ z)                    ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨
-    (x ∙ (x ◦ y)) ∙ (y ◦ z)        ≈⟨  ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩
+    x ∙ (y ◦ z)                    ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨
+    (x ∙ (x ◦ y)) ∙ (y ◦ z)        ≈⟨  ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩
     (x ∙ (y ◦ x)) ∙ (y ◦ z)        ≈⟨  ∙-assoc _ _ _ ⟩
-    x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨
-    x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨
+    x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨
+    x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨
     (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
     (x ∙ y) ◦ (x ∙ z)              ∎
 
@@ -284,15 +302,19 @@ module _ {_+_ _*_ : Op₂ A}
          (*-cong : Congruent₂ _*_)
          where
 
+  open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)
+
+  open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ)
+
   assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ →
                                 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                 LeftZero 0# _*_
   assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ  x = begin
-    0# * x                                 ≈⟨ sym (idʳ _) ⟩
-    (0# * x) + 0#                          ≈⟨ +-cong refl (sym (invʳ _)) ⟩
-    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
-    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩
-    ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩
+    0# * x                                 ≈⟨ idʳ _ ⟨
+    (0# * x) + 0#                          ≈⟨ +-congˡ (invʳ _) ⟨
+    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-congʳ (distribʳ _ _ _) ⟨
+    ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩
     (0# * x) + ((0# * x)⁻¹)                ≈⟨ invʳ _ ⟩
     0#                                     ∎
 
@@ -300,11 +322,11 @@ module _ {_+_ _*_ : Op₂ A}
                                 RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ →
                                 RightZero 0# _*_
   assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ  x = begin
-     x * 0#                                ≈⟨ sym (idʳ _) ⟩
-     (x * 0#) + 0#                         ≈⟨ +-cong refl (sym (invʳ _)) ⟩
-     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ sym (+-assoc _ _ _) ⟩
-     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩
-     (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩
+     x * 0#                                ≈⟨ idʳ _ ⟨
+     (x * 0#) + 0#                         ≈⟨ +-congˡ (invʳ _) ⟨
+     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-congʳ (distribˡ _ _ _) ⟨
+     (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩
      ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
      0#                                    ∎
 

From a6710a07cc73921f0f81b293d7654d2571c96798 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 13 Feb 2025 23:19:33 +0000
Subject: [PATCH 04/25] fix: knock-on DRY

---
 src/Algebra/Structures.agda | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda
index 1aae80d1cc..d56f194aad 100644
--- a/src/Algebra/Structures.agda
+++ b/src/Algebra/Structures.agda
@@ -54,13 +54,14 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
 
   setoid : Setoid a ℓ
   setoid = record { isEquivalence = isEquivalence }
-
+{-
   ∙-congˡ : LeftCongruent ∙
   ∙-congˡ y≈z = ∙-cong refl y≈z
 
   ∙-congʳ : RightCongruent ∙
   ∙-congʳ y≈z = ∙-cong y≈z refl
-
+-}
+  open Consequences.Congruence setoid ∙-cong public
 
 record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field

From 02a2d5ac484736181ef50ab05799ab2854d9c576 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 13 Feb 2025 23:47:54 +0000
Subject: [PATCH 05/25] fix: `CHANGELOG` plus cosmetics

---
 CHANGELOG.md                       | 10 ++++++++++
 src/Algebra/Consequences/Base.agda |  2 +-
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a99bafe7b7..3a4f4efd28 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -80,6 +80,16 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
+  ```
+
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  module Congruence (cong : Congruent₂ _≈_ _∙_)
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 048302f597..979a250865 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -13,9 +13,9 @@ module Algebra.Consequences.Base
 open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
-open import Relation.Binary.Core
 open import Relation.Binary.Consequences
   using (mono₂⇒monoˡ; mono₂⇒monoʳ)
+open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 
 module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) where

From d9c1136c1075fe93520efce95ef0acc147389419 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 08:13:10 +0000
Subject: [PATCH 06/25] refactor: change implicit to explicit

---
 src/Relation/Binary/Consequences.agda | 19 ++++++++++---------
 src/Relation/Binary/Definitions.agda  |  4 ++--
 2 files changed, 12 insertions(+), 11 deletions(-)

diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index bfa8a782a5..77fd23ea18 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -106,18 +106,19 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃}
 
 module _ {≤₁ : Rel A ℓ₁} {≤₂ : Rel B ℓ₂} {≤₃ : Rel C ℓ₂} where
 
-  mono₂⇒monoˡ : Reflexive ≤₁ →
-                ∀ {f} → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
-  mono₂⇒monoˡ refl mono = mono refl
+  mono₂⇒monoˡ : ∀ {f} → Reflexive ≤₁ →
+                Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
+  mono₂⇒monoˡ refl mono _ = mono refl
 
-  mono₂⇒monoʳ : Reflexive ≤₂ →
-                ∀ {f} → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
-  mono₂⇒monoʳ refl mono = flip mono refl
+  mono₂⇒monoʳ : ∀ {f} → Reflexive ≤₂ →
+                Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
+  mono₂⇒monoʳ refl mono _ = flip mono refl
 
-  monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ →
-                      ∀ {f} → LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
+  monoˡ∧monoʳ⇒mono₂ : ∀ {f} → Transitive ≤₃ →
+                      LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
                       Monotonic₂ ≤₁ ≤₂ ≤₃ f
-  monoˡ∧monoʳ⇒mono₂ trans monoˡ monoʳ x≤₁y u≤₂v = trans (monoˡ u≤₂v) (monoʳ x≤₁y)
+  monoˡ∧monoʳ⇒mono₂ trans monoˡ monoʳ x≤₁y u≤₂v =
+    trans (monoˡ _ u≤₂v) (monoʳ _ x≤₁y)
 
 ------------------------------------------------------------------------
 -- Proofs for strict orders
diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda
index 95ed9a18ac..e3fe520782 100644
--- a/src/Relation/Binary/Definitions.agda
+++ b/src/Relation/Binary/Definitions.agda
@@ -158,10 +158,10 @@ Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
 Antitonic₁ _≤_ = Monotonic₁ (flip _≤_)
 
 LeftMonotonic : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
-LeftMonotonic _≤_ _⊑_ _∙_ = ∀ {x} → Monotonic₁ _≤_ _⊑_ (x ∙_)
+LeftMonotonic _≤_ _⊑_ _∙_ = ∀ x → Monotonic₁ _≤_ _⊑_ (x ∙_)
 
 RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
-RightMonotonic _≤_ _⊑_ _∙_ = ∀ {y} → Monotonic₁ _≤_ _⊑_ (_∙ y)
+RightMonotonic _≤_ _⊑_ _∙_ = ∀ y → Monotonic₁ _≤_ _⊑_ (_∙ y)
 
 Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
 Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_

From c17597026383d332c035e24ee7573c8214e9fc14 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 08:13:38 +0000
Subject: [PATCH 07/25] fix: make `CHANGELOG` more detailed

---
 CHANGELOG.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3a4f4efd28..474f727bca 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -82,12 +82,16 @@ Additions to existing modules
 
 * In `Algebra.Consequences.Base`:
   ```agda
-  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
+  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
+    congˡ : LeftCongruent _≈_ _∙_
+    congʳ : RightCongruent _≈_ _∙_
   ```
 
 * In `Algebra.Consequences.Setoid`:
   ```agda
   module Congruence (cong : Congruent₂ _≈_ _∙_)
+    ∙-congˡ : LeftCongruent _≈_ _∙_
+    ∙-congʳ : RightCongruent _≈_ _∙_
   ```
 
 * In `Algebra.Construct.Pointwise`:

From 84c579c34e461f067e00a91119328f073b2faccf Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 08:17:40 +0000
Subject: [PATCH 08/25] refactor: rectify the names

---
 CHANGELOG.md                         | 6 +++---
 src/Algebra/Consequences/Base.agda   | 8 ++++----
 src/Algebra/Consequences/Setoid.agda | 1 -
 3 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 474f727bca..b19f211e0d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -83,13 +83,13 @@ Additions to existing modules
 * In `Algebra.Consequences.Base`:
   ```agda
   module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
-    congˡ : LeftCongruent _≈_ _∙_
-    congʳ : RightCongruent _≈_ _∙_
+    ∙-congˡ : LeftCongruent _≈_ _∙_
+    ∙-congʳ : RightCongruent _≈_ _∙_
   ```
 
 * In `Algebra.Consequences.Setoid`:
   ```agda
-  module Congruence (cong : Congruent₂ _≈_ _∙_)
+  module Congruence (cong : Congruent₂ _≈_ _∙_) where
     ∙-congˡ : LeftCongruent _≈_ _∙_
     ∙-congʳ : RightCongruent _≈_ _∙_
   ```
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 979a250865..570c26eb03 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -25,11 +25,11 @@ module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) where
 
   module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
 
-    congˡ : LeftCongruent _≈_ _∙_
-    congˡ = mono₂⇒monoˡ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong
+    ∙-congˡ : LeftCongruent _≈_ _∙_
+    ∙-congˡ = mono₂⇒monoˡ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong _
 
-    congʳ : RightCongruent _≈_ _∙_
-    congʳ = mono₂⇒monoʳ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong
+    ∙-congʳ : RightCongruent _≈_ _∙_
+    ∙-congʳ = mono₂⇒monoʳ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong _
 
 module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
 
diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
index 9b90eba41a..683d2e87c7 100644
--- a/src/Algebra/Consequences/Setoid.agda
+++ b/src/Algebra/Consequences/Setoid.agda
@@ -40,7 +40,6 @@ open Base public
 module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 
   open Base.Congruence _≈_ cong refl public
-    renaming (congˡ to ∙-congˡ; congʳ to ∙-congʳ)
 
 ------------------------------------------------------------------------
 -- MiddleFourExchange

From 0ffa707938155a681afa9b1d1437dd0843554885 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 08:36:22 +0000
Subject: [PATCH 09/25] refactor: use the new definitions

---
 src/Data/Nat/Properties.agda | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 20428045ea..41705eeff6 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -38,9 +38,13 @@ open import Level using (0ℓ)
 open import Relation.Unary as U using (Pred)
 open import Relation.Binary.Core
   using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary
-open import Relation.Binary.Consequences using (flip-Connex)
+open import Relation.Binary.Bundles
+open import Relation.Binary.Definitions
+open import Relation.Binary.Consequences
+  using (mono₂⇒monoˡ; mono₂⇒monoʳ; flip-Connex)
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Structures
+open import Relation.Binary.Structures.Biased
 open import Relation.Nullary hiding (Irrelevant)
 open import Relation.Nullary.Decidable using (True; via-injection; map′; recompute)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
@@ -702,15 +706,15 @@ m+n≤o⇒n≤o : ∀ m {n o} → m + n ≤ o → n ≤ o
 m+n≤o⇒n≤o zero    n≤o   = n≤o
 m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 
-+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
++-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
 +-mono-≤ {_} {m} z≤n       o≤p = ≤-trans o≤p (m≤n+m _ m)
 +-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)
 
-+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
-+-monoˡ-≤ n m≤o = +-mono-≤ m≤o (≤-refl {n})
++-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
++-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl +-mono-≤
 
-+-monoʳ-≤ : ∀ n → (n +_) Preserves _≤_ ⟶ _≤_
-+-monoʳ-≤ n m≤o = +-mono-≤ (≤-refl {n}) m≤o
++-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
++-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl +-mono-≤
 
 +-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
 +-mono-<-≤ {_} {suc n} z<s               o≤p = s≤s (m≤n⇒m≤o+n n o≤p)

From 54b310d95585a40ebf4b79e277f0d09eb8a41686 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 09:08:24 +0000
Subject: [PATCH 10/25] refactor: use the new definitions some more

---
 src/Data/Nat/Properties.agda | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 41705eeff6..415e275015 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -716,21 +716,21 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 +-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
 +-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl +-mono-≤
 
-+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
++-mono-<-≤ : Monotonic₂ _<_ _≤_ _<_ _+_
 +-mono-<-≤ {_} {suc n} z<s               o≤p = s≤s (m≤n⇒m≤o+n n o≤p)
 +-mono-<-≤ {_} {_}     (s<s m<n@(s≤s _)) o≤p = s≤s (+-mono-<-≤ m<n o≤p)
 
-+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
++-mono-≤-< : Monotonic₂ _≤_ _<_ _<_ _+_
 +-mono-≤-< {_} {n} z≤n       o<p = ≤-trans o<p (m≤n+m _ n)
 +-mono-≤-< {_} {_} (s≤s m≤n) o<p = s≤s (+-mono-≤-< m≤n o<p)
 
-+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
++-mono-< : Monotonic₂ _<_ _<_ _<_ _+_
 +-mono-< m≤n = +-mono-≤-< (<⇒≤ m≤n)
 
-+-monoˡ-< : ∀ n → (_+ n) Preserves _<_ ⟶ _<_
++-monoˡ-< : RightMonotonic _<_ _<_ _+_
 +-monoˡ-< n = +-monoˡ-≤ n
 
-+-monoʳ-< : ∀ n → (n +_) Preserves _<_ ⟶ _<_
++-monoʳ-< : LeftMonotonic _<_ _<_ _+_
 +-monoʳ-< zero    m≤o = m≤o
 +-monoʳ-< (suc n) m≤o = s≤s (+-monoʳ-< n m≤o)
 
@@ -972,25 +972,25 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-cancelˡ-≤ : ∀ o .{{_ : NonZero o}} → o * m ≤ o * n → m ≤ n
 *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
 
-*-mono-≤ : _*_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
+*-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _*_
 *-mono-≤ z≤n       _   = z≤n
 *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
-*-monoˡ-≤ : ∀ n → (_* n) Preserves _≤_ ⟶ _≤_
-*-monoˡ-≤ n m≤o = *-mono-≤ m≤o (≤-refl {n})
+*-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
+*-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
 
-*-monoʳ-≤ : ∀ n → (n *_) Preserves _≤_ ⟶ _≤_
-*-monoʳ-≤ n m≤o = *-mono-≤ (≤-refl {n}) m≤o
+*-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
+*-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl *-mono-≤
 
-*-mono-< : _*_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+*-mono-< : Monotonic₂ _<_ _<_ _<_ _*_
 *-mono-< z<s               u<v@(s≤s _) = 0<1+n
 *-mono-< (s<s m<n@(s≤s _)) u<v@(s≤s _) = +-mono-< u<v (*-mono-< m<n u<v)
 
-*-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_* n) Preserves _<_ ⟶ _<_
+*-monoˡ-< : ∀ n .{{_ : NonZero n}} → Monotonic₁ _<_ _<_ (_* n)
 *-monoˡ-< n@(suc _) z<s               = 0<1+n
 *-monoˡ-< n@(suc _) (s<s m<o@(s≤s _)) = +-mono-≤-< ≤-refl (*-monoˡ-< n m<o)
 
-*-monoʳ-< : ∀ n .{{_ : NonZero n}} → (n *_) Preserves _<_ ⟶ _<_
+*-monoʳ-< : ∀ n .{{_ : NonZero n}} → Monotonic₁ _<_ _<_ (n *_)
 *-monoʳ-< (suc zero)      m<o@(s≤s _) = +-mono-≤ m<o z≤n
 *-monoʳ-< (suc n@(suc _)) m<o@(s≤s _) = +-mono-≤ m<o (<⇒≤ (*-monoʳ-< n m<o))
 
@@ -1093,19 +1093,19 @@ m^n≢0 m n = ≢-nonZero (≢-nonZero⁻¹ m ∘′ m^n≡0⇒m≡0 m n)
 m^n>0 : ∀ m .{{_ : NonZero m}} n → m ^ n > 0
 m^n>0 m n = >-nonZero⁻¹ (m ^ n) {{m^n≢0 m n}}
 
-^-monoˡ-≤ : ∀ n → (_^ n) Preserves _≤_ ⟶ _≤_
+^-monoˡ-≤ : RightMonotonic _≤_ _≤_ _^_
 ^-monoˡ-≤ zero m≤o = s≤s z≤n
 ^-monoˡ-≤ (suc n) m≤o = *-mono-≤ m≤o (^-monoˡ-≤ n m≤o)
 
-^-monoʳ-≤ : ∀ m .{{_ : NonZero m}} → (m ^_) Preserves _≤_ ⟶ _≤_
+^-monoʳ-≤ : ∀ m .{{_ : NonZero m}} → Monotonic₁ _≤_ _≤_ (m ^_)
 ^-monoʳ-≤ m {_} {o} z≤n = n≢0⇒n>0 (≢-nonZero⁻¹ (m ^ o) {{m^n≢0 m o}})
 ^-monoʳ-≤ m (s≤s n≤o) = *-monoʳ-≤ m (^-monoʳ-≤ m n≤o)
 
-^-monoˡ-< : ∀ n .{{_ : NonZero n}} → (_^ n) Preserves _<_ ⟶ _<_
+^-monoˡ-< : ∀ n .{{_ : NonZero n}} → Monotonic₁ _<_ _<_ (_^ n)
 ^-monoˡ-< (suc zero)      m<o = *-monoˡ-< 1 m<o
 ^-monoˡ-< (suc n@(suc _)) m<o = *-mono-< m<o (^-monoˡ-< n m<o)
 
-^-monoʳ-< : ∀ m → 1 < m → (m ^_) Preserves _<_ ⟶ _<_
+^-monoʳ-< : ∀ m → 1 < m → Monotonic₁ _<_ _<_ (m ^_)
 ^-monoʳ-< m@(suc _) 1<m {zero}  {suc o} z<s       = *-mono-≤ 1<m (m^n>0 m o)
 ^-monoʳ-< m@(suc _) 1<m {suc n} {suc o} (s<s n<o) = *-monoʳ-< m (^-monoʳ-< m 1<m n<o)
 

From f18f031e06d5ab935895a769c7016c835b8e4f99 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 09:45:46 +0000
Subject: [PATCH 11/25] refactor: use the new definitions some more

---
 src/Data/Nat/Properties.agda          | 4 ++--
 src/Relation/Binary/Consequences.agda | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 415e275015..b40e244d16 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -973,14 +973,14 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-cancelˡ-≤ {m} {n} o rewrite *-comm o m | *-comm o n = *-cancelʳ-≤ m n o
 
 *-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _*_
-*-mono-≤ z≤n       _   = z≤n
+*-mono-≤ z≤n       u≤v = z≤n
 *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
 *-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
 *-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
 
 *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
-*-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl *-mono-≤
+*-monoʳ-≤ m {x} {y} x≤y = mono₂⇒monoˡ {≤₂ = _≤_} {≤₃ = _≤_} {f = _*_} ≤-refl *-mono-≤ m x≤y --  {≤₃ = _≤_} ≤-refl *-mono-≤ m
 
 *-mono-< : Monotonic₂ _<_ _<_ _<_ _*_
 *-mono-< z<s               u<v@(s≤s _) = 0<1+n
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index 77fd23ea18..bd59bf053f 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -108,11 +108,11 @@ module _ {≤₁ : Rel A ℓ₁} {≤₂ : Rel B ℓ₂} {≤₃ : Rel C ℓ₂}
 
   mono₂⇒monoˡ : ∀ {f} → Reflexive ≤₁ →
                 Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
-  mono₂⇒monoˡ refl mono _ = mono refl
+  mono₂⇒monoˡ refl mono x = mono (refl {x = x})
 
   mono₂⇒monoʳ : ∀ {f} → Reflexive ≤₂ →
                 Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
-  mono₂⇒monoʳ refl mono _ = flip mono refl
+  mono₂⇒monoʳ refl mono y = flip mono (refl {x = y})
 
   monoˡ∧monoʳ⇒mono₂ : ∀ {f} → Transitive ≤₃ →
                       LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →

From 7bc97cec224f6fad9a38cdb77c2f9be7625149b0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 09:53:54 +0000
Subject: [PATCH 12/25] refactor: unsolved metas make this a pain!

---
 src/Data/Nat/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b40e244d16..c0dccce51b 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -977,10 +977,10 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
 *-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
-*-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
+*-monoˡ-≤ = mono₂⇒monoʳ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
 
 *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
-*-monoʳ-≤ m {x} {y} x≤y = mono₂⇒monoˡ {≤₂ = _≤_} {≤₃ = _≤_} {f = _*_} ≤-refl *-mono-≤ m x≤y --  {≤₃ = _≤_} ≤-refl *-mono-≤ m
+*-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
 
 *-mono-< : Monotonic₂ _<_ _<_ _<_ _*_
 *-mono-< z<s               u<v@(s≤s _) = 0<1+n

From 0cb6671f85d08b79f6a0c51e8dc351e2394e20b7 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 14 Feb 2025 17:15:32 +0000
Subject: [PATCH 13/25] refactor: use the new definitions

---
 src/Data/Integer/Properties.agda | 57 ++++++++++++++++----------------
 1 file changed, 29 insertions(+), 28 deletions(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index f89d3164f6..9eaa83c42a 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -28,6 +28,7 @@ import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
+open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂; LeftMonotonic; RightMonotonic)
 open import Relation.Binary.Bundles using
   (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder)
 open import Relation.Binary.Structures
@@ -414,7 +415,7 @@ neg-≤-pos : ∀ {m n} → - (+ m) ≤ + n
 neg-≤-pos {zero}  = +≤+ z≤n
 neg-≤-pos {suc m} = -≤+
 
-neg-mono-≤ : -_ Preserves _≤_ ⟶ _≥_
+neg-mono-≤ : Monotonic₁ _≤_ _≥_ (-_)
 neg-mono-≤ -≤+             = neg-≤-pos
 neg-mono-≤ (-≤- n≤m)       = +≤+ (s≤s n≤m)
 neg-mono-≤ (+≤+ z≤n)       = neg-≤-pos
@@ -429,7 +430,7 @@ neg-cancel-≤ { +0}       { -[1+ n ]}  _               = -≤+
 neg-cancel-≤ { -[1+ m ]} { +0}        (+≤+ ())
 neg-cancel-≤ { -[1+ m ]} { -[1+ n ]}  (+≤+ (s≤s m≤n)) = -≤- m≤n
 
-neg-mono-< : -_ Preserves _<_ ⟶ _>_
+neg-mono-< : Monotonic₁ _<_ _>_ (-_)
 neg-mono-< { -[1+ _ ]} { -[1+ _ ]} (-<- n<m) = +<+ (s<s n<m)
 neg-mono-< { -[1+ _ ]} { +0}       -<+       = +<+ z<s
 neg-mono-< { -[1+ _ ]} { +[1+ n ]} -<+       = -<+
@@ -745,7 +746,7 @@ sign-⊖-< {suc m} {suc n} (ℕ.s<s m<n) = begin
 sign-⊖-≰ : n ℕ.≰ m → sign (m ⊖ n) ≡ Sign.-
 sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
 
-⊖-monoʳ-≥-≤ : ∀ n → (n ⊖_) Preserves ℕ._≥_ ⟶ _≤_
+⊖-monoʳ-≥-≤ : LeftMonotonic ℕ._≥_ _≤_ _⊖_
 ⊖-monoʳ-≥-≤ zero    {m}     z≤n      = 0⊖m≤+ m
 ⊖-monoʳ-≥-≤ zero    {_}    (s≤s m≤n) = -≤- m≤n
 ⊖-monoʳ-≥-≤ (suc n) {zero}  z≤n      = ≤-refl
@@ -759,7 +760,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
   n ⊖ o         ≡⟨ [1+m]⊖[1+n]≡m⊖n n o ⟨
   suc n ⊖ suc o ∎ where open ≤-Reasoning
 
-⊖-monoˡ-≤ : ∀ n → (_⊖ n) Preserves ℕ._≤_ ⟶ _≤_
+⊖-monoˡ-≤ : RightMonotonic ℕ._≤_ _≤_ _⊖_
 ⊖-monoˡ-≤ zero    {_} {_}     m≤o = +≤+ m≤o
 ⊖-monoˡ-≤ (suc n) {_} {0}     z≤n = ≤-refl
 ⊖-monoˡ-≤ (suc n) {_} {suc o} z≤n = begin
@@ -1027,7 +1028,7 @@ neg-distrib-+ -[1+ m ]  (+   n)   =
 ------------------------------------------------------------------------
 -- Properties of _+_ and _≤_
 
-+-monoʳ-≤ : ∀ n → (_+_ n) Preserves _≤_ ⟶ _≤_
++-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
 +-monoʳ-≤ (+ n)    {_}         (-≤- o≤m) = ⊖-monoʳ-≥-≤ n (s≤s o≤m)
 +-monoʳ-≤ (+ n)    { -[1+ m ]} -≤+       = ≤-trans (m⊖n≤m n (suc m)) (+≤+ (ℕ.m≤m+n n _))
 +-monoʳ-≤ (+ n)    {_}         (+≤+ m≤o) = +≤+ (ℕ.+-monoʳ-≤ n m≤o)
@@ -1035,7 +1036,7 @@ neg-distrib-+ -[1+ m ]  (+   n)   =
 +-monoʳ-≤ -[1+ n ] {_} {+ m}   -≤+       = ≤-trans (-≤- (ℕ.m≤m+n (suc n) _)) (-1+m≤n⊖m (suc n) m)
 +-monoʳ-≤ -[1+ n ] {_} {_}     (+≤+ m≤n) = ⊖-monoˡ-≤ (suc n) m≤n
 
-+-monoˡ-≤ : ∀ n → (_+ n) Preserves _≤_ ⟶ _≤_
++-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
 +-monoˡ-≤ n {i} {j} rewrite +-comm i n | +-comm j n = +-monoʳ-≤ n
 
 +-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
@@ -1057,7 +1058,7 @@ i≤i+j i j rewrite +-comm i j = i≤j+i i j
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
-+-monoʳ-< : ∀ i → (_+_ i) Preserves _<_ ⟶ _<_
++-monoʳ-< : LeftMonotonic _<_ _<_ _+_
 +-monoʳ-< (+ n)    {_} {_}   (-<- o<m) = ⊖-monoʳ->-< n (s<s o<m)
 +-monoʳ-< (+ n)    {_} {_}   -<+       = <-≤-trans (m⊖1+n<m n _) (+≤+ (ℕ.m≤m+n n _))
 +-monoʳ-< (+ n)    {_} {_}   (+<+ m<o) = +<+ (ℕ.+-monoʳ-< n m<o)
@@ -1065,20 +1066,20 @@ i≤i+j i j rewrite +-comm i j = i≤j+i i j
 +-monoʳ-< -[1+ n ] {_} {+ o} -<+       = <-≤-trans (-<- (ℕ.m≤m+n (suc n) _)) (-[1+m]≤n⊖m+1 n o)
 +-monoʳ-< -[1+ n ] {_} {_}   (+<+ m<o) = ⊖-monoˡ-< (suc n) m<o
 
-+-monoˡ-< : ∀ i → (_+ i) Preserves _<_ ⟶ _<_
++-monoˡ-< : RightMonotonic _<_ _<_ _+_
 +-monoˡ-< i {j} {k} rewrite +-comm j i | +-comm k i = +-monoʳ-< i
 
-+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
++-mono-< : Monotonic₂ _<_ _<_ _<_ _+_
 +-mono-< {i} {j} {k} {l} i<j k<l = begin-strict
   i + k <⟨ +-monoˡ-< k i<j ⟩
   j + k <⟨ +-monoʳ-< j k<l ⟩
   j + l ∎
   where open ≤-Reasoning
 
-+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
++-mono-≤-< : Monotonic₂ _≤_ _<_ _<_ _+_
 +-mono-≤-< {i} {j} {k} i≤j j<k = ≤-<-trans (+-monoˡ-≤ k i≤j) (+-monoʳ-< j j<k)
 
-+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
++-mono-<-≤ : Monotonic₂ _<_ _≤_ _<_ _+_
 +-mono-<-≤ {i} {j} {k} i<j j≤k = <-≤-trans (+-monoˡ-< k i<j) (+-monoʳ-≤ j j≤k)
 
 ------------------------------------------------------------------------
@@ -1226,7 +1227,7 @@ i≢suc[i] { -[1+ suc n ]} ()
 1-[1+n]≡-n zero    = refl
 1-[1+n]≡-n (suc n) = refl
 
-suc-mono : sucℤ Preserves _≤_ ⟶ _≤_
+suc-mono : Monotonic₁ _≤_ _≤_ sucℤ
 suc-mono (-≤+ {m} {n}) = begin
   1 ⊖ suc m  ≡⟨ [1+m]⊖[1+n]≡m⊖n 0 m ⟩
   0 ⊖ m      ≤⟨ 0⊖m≤+ m ⟩
@@ -1719,7 +1720,7 @@ neg-distribʳ-* i j = begin
 *-cancelˡ-≤-pos : ∀ i j k .{{_ : Positive k}} → k * i ≤ k * j → i ≤ j
 *-cancelˡ-≤-pos i j k rewrite *-comm k i | *-comm k j = *-cancelʳ-≤-pos i j k
 
-*-monoʳ-≤-nonNeg : ∀ i .{{_ : NonNegative i}} → (_* i) Preserves _≤_ ⟶ _≤_
+*-monoʳ-≤-nonNeg : ∀ i .{{_ : NonNegative i}} → Monotonic₁ _≤_ _≤_ (_* i)
 *-monoʳ-≤-nonNeg +0 {i} {j} i≤j rewrite *-zeroʳ i | *-zeroʳ j = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = 0})         = -≤+
 *-monoʳ-≤-nonNeg +[1+ n ] (-≤+ {n = suc _})     = -≤+
@@ -1728,7 +1729,7 @@ neg-distribʳ-* i j = begin
 *-monoʳ-≤-nonNeg +[1+ n ] {+0}       {+[1+ _ ]} (+≤+ m≤n) = +≤+ z≤n
 *-monoʳ-≤-nonNeg +[1+ n ] {+[1+ _ ]} {+[1+ _ ]} (+≤+ m≤n) = +≤+ (ℕ.*-monoˡ-≤ (suc n) m≤n)
 
-*-monoˡ-≤-nonNeg : ∀ i .{{_ : NonNegative i}} → (i *_) Preserves _≤_ ⟶ _≤_
+*-monoˡ-≤-nonNeg : ∀ i .{{_ : NonNegative i}} → Monotonic₁ _≤_ _≤_ (i *_)
 *-monoˡ-≤-nonNeg i {j} {k} rewrite *-comm i j | *-comm i k = *-monoʳ-≤-nonNeg i
 
 *-cancelˡ-≤-neg : ∀ i j k .{{_ : Negative i}} → i * j ≤ i * k → j ≥ k
@@ -1744,7 +1745,7 @@ neg-distribʳ-* i j = begin
 *-cancelʳ-≤-neg : ∀ i j k .{{_ : Negative k}} → i * k ≤ j * k → i ≥ j
 *-cancelʳ-≤-neg i j k rewrite *-comm i k | *-comm j k = *-cancelˡ-≤-neg k i j
 
-*-monoˡ-≤-nonPos : ∀ i .{{_ : NonPositive i}} → (i *_) Preserves _≤_ ⟶ _≥_
+*-monoˡ-≤-nonPos : ∀ i .{{_ : NonPositive i}} → Monotonic₁ _≤_ _≥_ (i *_)
 *-monoˡ-≤-nonPos +0           {j} {k} j≤k = +≤+ z≤n
 *-monoˡ-≤-nonPos i@(-[1+ m ]) {j} {k} j≤k = begin
   i * k        ≡⟨ neg-distribˡ-* (- i) k ⟨
@@ -1755,18 +1756,18 @@ neg-distribʳ-* i j = begin
   i * j        ∎
   where open ≤-Reasoning
 
-*-monoʳ-≤-nonPos : ∀ i .{{_ : NonPositive i}} → (_* i) Preserves _≤_ ⟶ _≥_
+*-monoʳ-≤-nonPos : ∀ i .{{_ : NonPositive i}} → Monotonic₁ _≤_ _≥_ (_* i)
 *-monoʳ-≤-nonPos i {j} {k} rewrite *-comm k i | *-comm j i = *-monoˡ-≤-nonPos i
 
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
-*-monoˡ-<-pos : ∀ i .{{_ : Positive i}} → (i *_) Preserves _<_ ⟶ _<_
+*-monoˡ-<-pos : ∀ i .{{_ : Positive i}} → Monotonic₁ _<_ _<_ (i *_)
 *-monoˡ-<-pos +[1+ n ] {+ m}       {+ o}       (+<+ m<o) = +◃-mono-< (ℕ.+-mono-<-≤ m<o (ℕ.*-monoʳ-≤ n (ℕ.<⇒≤ m<o)))
 *-monoˡ-<-pos +[1+ n ] { -[1+ m ]} {+ o}       leq       = -◃<+◃ _ (suc n ℕ.* o)
 *-monoˡ-<-pos +[1+ n ] { -[1+ m ]} { -[1+ o ]} (-<- o<m) = -<- (ℕ.+-mono-<-≤ o<m (ℕ.*-monoʳ-≤ n (ℕ.<⇒≤ (s≤s o<m))))
 
-*-monoʳ-<-pos : ∀ i .{{_ : Positive i}} → (_* i) Preserves _<_ ⟶ _<_
+*-monoʳ-<-pos : ∀ i .{{_ : Positive i}} → Monotonic₁ _<_ _<_ (_* i)
 *-monoʳ-<-pos i {j} {k} rewrite *-comm j i | *-comm k i = *-monoˡ-<-pos i
 
 *-cancelˡ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → k * i < k * j → i < j
@@ -1778,7 +1779,7 @@ neg-distribʳ-* i j = begin
 *-cancelʳ-<-nonNeg : ∀ k .{{_ : NonNegative k}} → i * k < j * k → i < j
 *-cancelʳ-<-nonNeg {i} {j} k rewrite *-comm i k | *-comm j k = *-cancelˡ-<-nonNeg k
 
-*-monoˡ-<-neg : ∀ i .{{_ : Negative i}} → (i *_) Preserves _<_ ⟶ _>_
+*-monoˡ-<-neg : ∀ i .{{_ : Negative i}} → Monotonic₁ _<_ _>_ (i *_)
 *-monoˡ-<-neg i@(-[1+ _ ]) {j} {k} j<k = begin-strict
   i * k        ≡⟨ neg-distribˡ-* (- i) k ⟨
   -(- i * k)   ≡⟨  neg-distribʳ-* (- i) k ⟩
@@ -1788,7 +1789,7 @@ neg-distribʳ-* i j = begin
   i * j        ∎
   where open ≤-Reasoning
 
-*-monoʳ-<-neg : ∀ i .{{_ : Negative i}} → (_* i) Preserves _<_ ⟶ _>_
+*-monoʳ-<-neg : ∀ i .{{_ : Negative i}} → Monotonic₁ _<_ _>_ (_* i)
 *-monoʳ-<-neg i {j} {k} rewrite *-comm k i | *-comm j i = *-monoˡ-<-neg i
 
 *-cancelˡ-<-nonPos : ∀ k .{{_ : NonPositive k}} → k * i < k * j → i > j
@@ -1962,41 +1963,41 @@ open ⊓-⊔-latticeProperties public
 ------------------------------------------------------------------------
 -- Other properties of _⊓_ and _⊔_
 
-mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j
 mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f)
 
-mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j
 mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f)
 
-antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j
 antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f)
 
-antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j
 antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f)
 
-mono-<-distrib-⊓ : ∀ f → f Preserves _<_ ⟶ _<_ → ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j
+mono-<-distrib-⊓ : ∀ f → Monotonic₁ _<_ _<_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊓ f j
 mono-<-distrib-⊓ f f-mono-< i j with <-cmp i j
 ... | tri< i<j _    _   = trans (cong f (i≤j⇒i⊓j≡i (<⇒≤ i<j))) (sym (i≤j⇒i⊓j≡i (<⇒≤ (f-mono-< i<j))))
 ... | tri≈ _   refl _   = trans (cong f (i≤j⇒i⊓j≡i ≤-refl))    (sym (i≤j⇒i⊓j≡i ≤-refl))
 ... | tri> _   _    i>j = trans (cong f (i≥j⇒i⊓j≡j (<⇒≤ i>j))) (sym (i≥j⇒i⊓j≡j (<⇒≤ (f-mono-< i>j))))
 
-mono-<-distrib-⊔ : ∀ f → f Preserves _<_ ⟶ _<_ → ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j
+mono-<-distrib-⊔ : ∀ f → Monotonic₁ _<_ _<_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊔ f j
 mono-<-distrib-⊔ f f-mono-< i j with <-cmp i j
 ... | tri< i<j _    _   = trans (cong f (i≤j⇒i⊔j≡j (<⇒≤ i<j))) (sym (i≤j⇒i⊔j≡j (<⇒≤ (f-mono-< i<j))))
 ... | tri≈ _   refl _   = trans (cong f (i≤j⇒i⊔j≡j ≤-refl))    (sym (i≤j⇒i⊔j≡j ≤-refl))
 ... | tri> _   _    i>j = trans (cong f (i≥j⇒i⊔j≡i (<⇒≤ i>j))) (sym (i≥j⇒i⊔j≡i (<⇒≤ (f-mono-< i>j))))
 
-antimono-<-distrib-⊔ : ∀ f  → f Preserves _<_ ⟶ _>_ → ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j
+antimono-<-distrib-⊔ : ∀ f  → Monotonic₁ _<_ _>_ f → ∀ i j → f (i ⊔ j) ≡ f i ⊓ f j
 antimono-<-distrib-⊔ f f-mono-< i j with <-cmp i j
 ... | tri< i<j _    _   = trans (cong f (i≤j⇒i⊔j≡j (<⇒≤ i<j))) (sym (i≥j⇒i⊓j≡j (<⇒≤ (f-mono-< i<j))))
 ... | tri≈ _   refl _   = trans (cong f (i≤j⇒i⊔j≡j ≤-refl))    (sym (i≥j⇒i⊓j≡j ≤-refl))
 ... | tri> _   _    i>j = trans (cong f (i≥j⇒i⊔j≡i (<⇒≤ i>j))) (sym (i≤j⇒i⊓j≡i (<⇒≤ (f-mono-< i>j))))
 
-antimono-<-distrib-⊓ : ∀ f → f Preserves _<_ ⟶ _>_ → ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j
+antimono-<-distrib-⊓ : ∀ f → Monotonic₁ _<_ _>_ f → ∀ i j → f (i ⊓ j) ≡ f i ⊔ f j
 antimono-<-distrib-⊓ f f-mono-< i j with <-cmp i j
 ... | tri< i<j _    _   = trans (cong f (i≤j⇒i⊓j≡i (<⇒≤ i<j))) (sym (i≥j⇒i⊔j≡i (<⇒≤ (f-mono-< i<j))))
 ... | tri≈ _   refl _   = trans (cong f (i≤j⇒i⊓j≡i ≤-refl))    (sym (i≥j⇒i⊔j≡i ≤-refl))

From 17f626d6ded45205e36e608b8cf0115e191ebb6e Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 16 Feb 2025 10:34:11 +0000
Subject: [PATCH 14/25] refactor: use the new definitions

---
 .../Rational/Unnormalised/Properties.agda     | 66 +++++++++----------
 1 file changed, 33 insertions(+), 33 deletions(-)

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 11e8d917b1..ddaeb4e018 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -37,7 +37,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
+  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>; Monotonic₁; Monotonic₂)
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
@@ -193,7 +193,7 @@ neg-involutive p rewrite neg-involutive-≡ p = ≃-refl
   ↥(- q) ℤ.* ↧ p            ∎)
   where open ≡-Reasoning
 
-neg-mono-< : -_ Preserves  _<_ ⟶ _>_
+neg-mono-< : Monotonic₁  _<_ _>_ (-_)
 neg-mono-< {p@record{}} {q@record{}} (*<* p<q) = *<* $ begin-strict
   ℤ.-  ↥ q ℤ.* ↧ p     ≡⟨ ℤ.neg-distribˡ-* (↥ q) (↧ p) ⟨
   ℤ.- (↥ q ℤ.* ↧ p)    <⟨ ℤ.neg-mono-< p<q ⟩
@@ -366,10 +366,10 @@ _≥?_ = flip _≤?_
 ------------------------------------------------------------------------
 -- Other properties of _≤_
 
-mono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≤_ → f Preserves _≃_ ⟶ _≃_
+mono⇒cong : ∀ {f} → Monotonic₁ _≤_ _≤_ f → Congruent₁ _≃_ f
 mono⇒cong = BC.mono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
 
-antimono⇒cong : ∀ {f} → f Preserves _≤_ ⟶ _≥_ → f Preserves _≃_ ⟶ _≃_
+antimono⇒cong : ∀ {f} → Monotonic₁ _≤_ _≥_ f → Congruent₁ _≃_ f
 antimono⇒cong = BC.antimono⇒cong _≃_ _≃_ ≃-sym ≤-reflexive ≤-antisym
 
 ------------------------------------------------------------------------
@@ -828,7 +828,7 @@ private
                       refl (↥ r) (↧ r) (↧ p) (↥ p) (↧ q)
     where open ℤ-solver
 
-+-monoʳ-≤ : ∀ r → (r +_) Preserves _≤_ ⟶ _≤_
++-monoʳ-≤ : ∀ r → Monotonic₁ _≤_ _≤_ (r +_)
 +-monoʳ-≤ r@record{} {p@record{}} {q@record{}} (*≤* x≤y) = *≤* $ begin
   ↥ (r + p) ℤ.* ↧ (r + q)                                  ≡⟨ lemma r p q ⟩
   r₂ ℤ.* (↧ p ℤ.* ↧ q) ℤ.+ (↧ r ℤ.* ↧ r) ℤ.* (↥ p ℤ.* ↧ q) ≤⟨ leq ⟩
@@ -840,10 +840,10 @@ private
     (ℤ.≤-reflexive $ cong (r₂ ℤ.*_) (ℤ.*-comm (↧ p) (↧ q)))
     (ℤ.*-monoˡ-≤-nonNeg (↧ r ℤ.* ↧ r) x≤y)
 
-+-monoˡ-≤ : ∀ r → (_+ r) Preserves _≤_ ⟶ _≤_
++-monoˡ-≤ : ∀ r → Monotonic₁ _≤_ _≤_ (_+ r)
 +-monoˡ-≤ r {p} {q} rewrite +-comm-≡ p r | +-comm-≡ q r = +-monoʳ-≤ r
 
-+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
++-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
 +-mono-≤ {p} {q} {u} {v} p≤q u≤v = ≤-trans (+-monoˡ-≤ u p≤q) (+-monoʳ-≤ q u≤v)
 
 p≤q⇒p≤r+q : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
@@ -858,7 +858,7 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
-+-monoʳ-< : ∀ r → (r +_) Preserves _<_ ⟶ _<_
++-monoʳ-< : ∀ r → Monotonic₁ _<_ _<_ (r +_)
 +-monoʳ-< r@record{} {p@record{}} {q@record{}} (*<* x<y) = *<* $ begin-strict
   ↥ (r + p) ℤ.* (↧ (r + q))                          ≡⟨ lemma r p q ⟩
   ↥r↧r ℤ.* (↧ p ℤ.* ↧ q) ℤ.+ ↧r↧r ℤ.* (↥ p ℤ.* ↧ q)  <⟨ leq ⟩
@@ -870,16 +870,16 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
     (ℤ.≤-reflexive $ cong (↥r↧r ℤ.*_) (ℤ.*-comm (↧ p) (↧ q)))
     (ℤ.*-monoˡ-<-pos ↧r↧r x<y)
 
-+-monoˡ-< : ∀ r → (_+ r) Preserves _<_ ⟶ _<_
++-monoˡ-< : ∀ r → Monotonic₁ _<_ _<_ (_+ r)
 +-monoˡ-< r {p} {q} rewrite +-comm-≡ p r | +-comm-≡ q r = +-monoʳ-< r
 
-+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
++-mono-< : Monotonic₂ _<_ _<_ _<_ _+_
 +-mono-< {p} {q} {u} {v} p<q u<v = <-trans (+-monoˡ-< u p<q) (+-monoʳ-< q u<v)
 
-+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
++-mono-≤-< : Monotonic₂ _≤_ _<_ _<_ _+_
 +-mono-≤-< {p} {q} {r} p≤q q<r = ≤-<-trans (+-monoˡ-≤ r p≤q) (+-monoʳ-< q q<r)
 
-+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
++-mono-<-≤ : Monotonic₂ _<_ _≤_ _<_ _+_
 +-mono-<-≤ {p} {q} {r} p<q q≤r = <-≤-trans (+-monoˡ-< r p<q) (+-monoʳ-≤ q q≤r)
 
 ------------------------------------------------------------------------
@@ -922,7 +922,7 @@ p-q≃0⇒p≃q p q p-q≃0 = begin-equality
   0ℚᵘ + q       ≡⟨ +-identityˡ-≡ q ⟩
   q             ∎ where open ≤-Reasoning
 
-neg-mono-≤ : -_ Preserves _≤_ ⟶ _≥_
+neg-mono-≤ : Monotonic₁ _≤_ _≥_ (-_)
 neg-mono-≤ {p@record{}} {q@record{}} (*≤* p≤q) = *≤* $ begin
   ℤ.- ↥ q ℤ.* ↧ p   ≡⟨ ℤ.neg-distribˡ-* (↥ q) (↧ p) ⟨
   ℤ.- (↥ q ℤ.* ↧ p) ≤⟨ ℤ.neg-mono-≤ p≤q ⟩
@@ -1248,7 +1248,7 @@ private
 *-cancelˡ-≤-neg : ∀ r .{{_ : Negative r}} → r * p ≤ r * q → q ≤ p
 *-cancelˡ-≤-neg {p} {q} r rewrite *-comm-≡ r p | *-comm-≡ r q = *-cancelʳ-≤-neg r
 
-*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_
+*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → Monotonic₁ _≤_ _≤_ (_* r)
 *-monoˡ-≤-nonNeg r@(mkℚᵘ (ℤ.+ n) _) {p@record{}} {q@record{}} (*≤* x<y) = *≤* $ begin
   ↥ p ℤ.* ↥ r ℤ.* (↧ q   ℤ.* ↧ r)  ≡⟨  reorder₂ (↥ p) _ _ _ ⟩
   l₁          ℤ.* (ℤ.+ n ℤ.* ↧ r)  ≡⟨  cong (l₁ ℤ.*_) (ℤ.pos-* n _) ⟨
@@ -1258,7 +1258,7 @@ private
   ↥ q ℤ.* ↥ r ℤ.* (↧ p   ℤ.* ↧ r)  ∎
   where open ℤ.≤-Reasoning; l₁ = ↥ p ℤ.* ↧ q ; l₂ = ↥ q ℤ.* ↧ p
 
-*-monoʳ-≤-nonNeg : ∀ r .{{_ :  NonNegative r}} → (r *_) Preserves _≤_ ⟶ _≤_
+*-monoʳ-≤-nonNeg : ∀ r .{{_ :  NonNegative r}} → Monotonic₁ _≤_ _≤_ (r *_)
 *-monoʳ-≤-nonNeg r {p} {q} rewrite *-comm-≡ r p | *-comm-≡ r q = *-monoˡ-≤-nonNeg r
 
 *-mono-≤-nonNeg : ∀ {p q r s} .{{_ : NonNegative p}} .{{_ : NonNegative r}} →
@@ -1269,7 +1269,7 @@ private
   q * s ∎
   where open ≤-Reasoning
 
-*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (_* r) Preserves _≤_ ⟶ _≥_
+*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → Monotonic₁ _≤_ _≥_ (_* r)
 *-monoˡ-≤-nonPos r {p} {q} p≤q = begin
   q * r        ≃⟨ neg-involutive (q * r) ⟨
   - - (q * r)  ≃⟨  -‿cong (neg-distribʳ-* q r) ⟩
@@ -1279,20 +1279,20 @@ private
   p * r        ∎
   where open ≤-Reasoning; -r≥0 = nonNegative (neg-mono-≤ (nonPositive⁻¹ r))
 
-*-monoʳ-≤-nonPos : ∀ r .{{_ :  NonPositive r}} → (r *_) Preserves _≤_ ⟶ _≥_
+*-monoʳ-≤-nonPos : ∀ r .{{_ :  NonPositive r}} → Monotonic₁ _≤_ _≥_ (r *_)
 *-monoʳ-≤-nonPos r {p} {q} rewrite *-comm-≡ r q | *-comm-≡ r p = *-monoˡ-≤-nonPos r
 
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
-*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → (_* r) Preserves _<_ ⟶ _<_
+*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → Monotonic₁ _<_ _<_ (_* r)
 *-monoˡ-<-pos r@record{} {p@record{}} {q@record{}} (*<* x<y) = *<* $ begin-strict
   ↥ p ℤ.*  ↥ r ℤ.* (↧ q  ℤ.* ↧ r) ≡⟨ reorder₁ (↥ p) _ _ _ ⟩
   ↥ p ℤ.*  ↧ q ℤ.*  ↥ r  ℤ.* ↧ r  <⟨ ℤ.*-monoʳ-<-pos (↧ r) (ℤ.*-monoʳ-<-pos (↥ r) x<y) ⟩
   ↥ q ℤ.*  ↧ p ℤ.*  ↥ r  ℤ.* ↧ r  ≡⟨ reorder₁ (↥ q) _ _ _ ⟨
   ↥ q ℤ.*  ↥ r ℤ.* (↧ p  ℤ.* ↧ r) ∎ where open ℤ.≤-Reasoning
 
-*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → (r *_) Preserves _<_ ⟶ _<_
+*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → Monotonic₁ _<_ _<_ (r *_)
 *-monoʳ-<-pos r {p} {q} rewrite *-comm-≡ r p | *-comm-≡ r q = *-monoˡ-<-pos r
 
 *-mono-<-nonNeg : ∀ {p q r s} .{{_ : NonNegative p}} .{{_ : NonNegative r}} →
@@ -1314,7 +1314,7 @@ private
 *-cancelˡ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → r * p < r * q → p < q
 *-cancelˡ-<-nonNeg {p} {q} r rewrite *-comm-≡ r p | *-comm-≡ r q = *-cancelʳ-<-nonNeg r
 
-*-monoˡ-<-neg : ∀ r .{{_ :  Negative r}} → (_* r) Preserves _<_ ⟶ _>_
+*-monoˡ-<-neg : ∀ r .{{_ :  Negative r}} → Monotonic₁ _<_ _>_ (_* r)
 *-monoˡ-<-neg r {p} {q} p<q = begin-strict
   q * r        ≃⟨ neg-involutive (q * r) ⟨
   - - (q * r)  ≃⟨ -‿cong (neg-distribʳ-* q r) ⟩
@@ -1324,7 +1324,7 @@ private
   p * r        ∎
   where open ≤-Reasoning; -r>0 = positive (neg-mono-< (negative⁻¹ r))
 
-*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → (r *_) Preserves _<_ ⟶ _>_
+*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (r *_)
 *-monoʳ-<-neg r {p} {q} rewrite *-comm-≡ r q | *-comm-≡ r p = *-monoˡ-<-neg r
 
 *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → q < p
@@ -1618,14 +1618,14 @@ open ⊓-⊔-properties public
   ; ⊔-triangulate             -- : ∀ p q r → p ⊔ q ⊔ r ≃ (p ⊔ q) ⊔ (q ⊔ r)
 
   ; ⊓-glb                     -- : ∀ {p q r} → p ≥ r → q ≥ r → p ⊓ q ≥ r
-  ; ⊓-mono-≤                  -- : _⊓_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
-  ; ⊓-monoˡ-≤                 -- : ∀ p → (_⊓ p) Preserves _≤_ ⟶ _≤_
-  ; ⊓-monoʳ-≤                 -- : ∀ p → (p ⊓_) Preserves _≤_ ⟶ _≤_
+  ; ⊓-mono-≤                  -- : Monotonic₂ _≤_ _≤_ _≤_ _⊓_
+  ; ⊓-monoˡ-≤                 -- : ∀ p → Monotonic₁_≤_ _≤_ (_⊓ p)
+  ; ⊓-monoʳ-≤                 -- : ∀ p → Monotonic₁_≤_ _≤_ (p ⊓_)
 
   ; ⊔-lub                     -- : ∀ {p q r} → p ≤ r → q ≤ r → p ⊔ q ≤ r
-  ; ⊔-mono-≤                  -- : _⊔_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
-  ; ⊔-monoˡ-≤                 -- : ∀ p → (_⊔ p) Preserves _≤_ ⟶ _≤_
-  ; ⊔-monoʳ-≤                 -- : ∀ p → (p ⊔_) Preserves _≤_ ⟶ _≤_
+  ; ⊔-mono-≤                  -- : Monotonic₂ _≤_ _≤_ _≤_ _⊔_
+  ; ⊔-monoˡ-≤                 -- : ∀ p → Monotonic₁_≤_ _≤_ (_⊔ p)
+  ; ⊔-monoʳ-≤                 -- : ∀ p → Monotonic₁_≤_ _≤_ (p ⊔_)
   )
   renaming
   ( x⊓y≈y⇒y≤x  to p⊓q≃q⇒q≤p      -- : ∀ {p q} → p ⊓ q ≃ q → q ≤ p
@@ -1682,19 +1682,19 @@ open ⊓-⊔-latticeProperties public
 ------------------------------------------------------------------------
 -- Monotonic or antimonotic functions distribute over _⊓_ and _⊔_
 
-mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ m n → f (m ⊔ n) ≃ f m ⊔ f n
 mono-≤-distrib-⊔ pres = ⊓-⊔-properties.mono-≤-distrib-⊔ (mono⇒cong pres) pres
 
-mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ m n → f (m ⊓ n) ≃ f m ⊓ f n
 mono-≤-distrib-⊓ pres = ⊓-⊔-properties.mono-≤-distrib-⊓ (mono⇒cong pres) pres
 
-antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ m n → f (m ⊓ n) ≃ f m ⊔ f n
 antimono-≤-distrib-⊓ pres = ⊓-⊔-properties.antimono-≤-distrib-⊓ (antimono⇒cong pres) pres
 
-antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ m n → f (m ⊔ n) ≃ f m ⊓ f n
 antimono-≤-distrib-⊔ pres = ⊓-⊔-properties.antimono-≤-distrib-⊔ (antimono⇒cong pres) pres
 
@@ -1740,12 +1740,12 @@ neg-distrib-⊓-⊔ = antimono-≤-distrib-⊓ neg-mono-≤
 ------------------------------------------------------------------------
 -- Properties of _⊓_, _⊔_ and _<_
 
-⊓-mono-< : _⊓_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+⊓-mono-< : Monotonic₂ _<_ _<_ _<_ _⊓_
 ⊓-mono-< {p} {r} {q} {s} p<r q<s with ⊓-sel r s
 ... | inj₁ r⊓s≃r = <-respʳ-≃ (≃-sym r⊓s≃r) (≤-<-trans (p⊓q≤p p q) p<r)
 ... | inj₂ r⊓s≃s = <-respʳ-≃ (≃-sym r⊓s≃s) (≤-<-trans (p⊓q≤q p q) q<s)
 
-⊔-mono-< : _⊔_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
+⊔-mono-< : Monotonic₂ _<_ _<_ _<_ _⊔_
 ⊔-mono-< {p} {r} {q} {s} p<r q<s with ⊔-sel p q
 ... | inj₁ p⊔q≃p = <-respˡ-≃ (≃-sym p⊔q≃p) (<-≤-trans p<r (p≤p⊔q r s))
 ... | inj₂ p⊔q≃q = <-respˡ-≃ (≃-sym p⊔q≃q) (<-≤-trans q<s (p≤q⊔p r s))

From 376c6da701cfbc9d8d984d692db4bcba35701207 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Sun, 16 Feb 2025 12:33:11 +0000
Subject: [PATCH 15/25] refactor: use the new lemma statements; not yet their
 generic proofs

---
 src/Data/Rational/Properties.agda             | 50 +++++++++----------
 .../Rational/Unnormalised/Properties.agda     |  6 +--
 2 files changed, 28 insertions(+), 28 deletions(-)

diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 0341f53c45..c47c0d1bbd 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -48,7 +48,7 @@ import Data.Rational.Unnormalised.Properties as ℚᵘ
 open import Data.Sum.Base as Sum using (inj₁; inj₂; [_,_]′; _⊎_)
 import Data.Sign.Base as Sign
 open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip)
-open import Function.Definitions using (Injective)
+open import Function.Definitions using (Congruent; Injective)
 open import Level using (0ℓ)
 open import Relation.Binary
 open import Relation.Binary.Morphism.Structures
@@ -442,10 +442,10 @@ fromℚᵘ-toℚᵘ (mkℚ (-[1+ n ]) d-1 c) = cong (-_) (normalize-coprime c)
 toℚᵘ-fromℚᵘ : ∀ p → toℚᵘ (fromℚᵘ p) ≃ᵘ p
 toℚᵘ-fromℚᵘ p = fromℚᵘ-injective (fromℚᵘ-toℚᵘ (fromℚᵘ p))
 
-toℚᵘ-cong : toℚᵘ Preserves _≡_ ⟶ _≃ᵘ_
+toℚᵘ-cong : Congruent _≡_ _≃ᵘ_ toℚᵘ
 toℚᵘ-cong refl = *≡* refl
 
-fromℚᵘ-cong : fromℚᵘ Preserves _≃ᵘ_ ⟶ _≡_
+fromℚᵘ-cong : Congruent _≃ᵘ_ _≡_ fromℚᵘ
 fromℚᵘ-cong {p} {q} p≃q = toℚᵘ-injective (begin-equality
   toℚᵘ (fromℚᵘ p)  ≃⟨  toℚᵘ-fromℚᵘ p ⟩
   p                ≃⟨  p≃q ⟩
@@ -998,7 +998,7 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
 ------------------------------------------------------------------------
 -- Properties of _+_ and _≤_
 
-+-mono-≤ : _+_ Preserves₂ _≤_ ⟶ _≤_ ⟶ _≤_
++-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
 +-mono-≤ {p} {q} {r} {s} p≤q r≤s = toℚᵘ-cancel-≤ (begin
   toℚᵘ(p + r)          ≃⟨ toℚᵘ-homo-+ p r ⟩
   toℚᵘ(p) ℚᵘ.+ toℚᵘ(r) ≤⟨ ℚᵘ.+-mono-≤ (toℚᵘ-mono-≤ p≤q) (toℚᵘ-mono-≤ r≤s) ⟩
@@ -1006,10 +1006,10 @@ neg-distrib-+ = +-Monomorphism.⁻¹-distrib-∙ ℚᵘ.+-0-isAbelianGroup (ℚ
   toℚᵘ(q + s)          ∎)
   where open ℚᵘ.≤-Reasoning
 
-+-monoˡ-≤ : ∀ r → (_+ r) Preserves _≤_ ⟶ _≤_
++-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
 +-monoˡ-≤ r p≤q = +-mono-≤ p≤q (≤-refl {r})
 
-+-monoʳ-≤ : ∀ r → (_+_ r) Preserves _≤_ ⟶ _≤_
++-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
 +-monoʳ-≤ r p≤q = +-mono-≤ (≤-refl {r}) p≤q
 
 nonNeg+nonNeg⇒nonNeg : ∀ p .{{_ : NonNegative p}} q .{{_ : NonNegative q}} → NonNegative (p + q)
@@ -1021,7 +1021,7 @@ nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonP
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
-+-mono-<-≤ : _+_ Preserves₂ _<_ ⟶ _≤_ ⟶ _<_
++-mono-<-≤ : Monotonic₂ _<_ _≤_ _<_ _+_
 +-mono-<-≤ {p} {q} {r} {s} p<q r≤s = toℚᵘ-cancel-< (begin-strict
   toℚᵘ(p + r)          ≃⟨ toℚᵘ-homo-+ p r ⟩
   toℚᵘ(p) ℚᵘ.+ toℚᵘ(r) <⟨ ℚᵘ.+-mono-<-≤ (toℚᵘ-mono-< p<q) (toℚᵘ-mono-≤ r≤s) ⟩
@@ -1029,16 +1029,16 @@ nonPos+nonPos⇒nonPos p q = nonPositive $ +-mono-≤ (nonPositive⁻¹ p) (nonP
   toℚᵘ(q + s)          ∎)
   where open ℚᵘ.≤-Reasoning
 
-+-mono-≤-< : _+_ Preserves₂ _≤_ ⟶ _<_ ⟶ _<_
++-mono-≤-< : Monotonic₂ _≤_ _<_ _<_ _+_
 +-mono-≤-< {p} {q} {r} {s} p≤q r<s rewrite +-comm p r | +-comm q s = +-mono-<-≤ r<s p≤q
 
-+-mono-< : _+_ Preserves₂ _<_ ⟶ _<_ ⟶ _<_
++-mono-< : Monotonic₂ _<_ _<_ _<_ _+_
 +-mono-< {p} {q} {r} {s} p<q r<s = <-trans (+-mono-<-≤ p<q (≤-refl {r})) (+-mono-≤-< (≤-refl {q}) r<s)
 
-+-monoˡ-< : ∀ r → (_+ r) Preserves _<_ ⟶ _<_
++-monoˡ-< : RightMonotonic _<_ _<_ _+_
 +-monoˡ-< r p<q = +-mono-<-≤ p<q (≤-refl {r})
 
-+-monoʳ-< : ∀ r → (_+_ r) Preserves _<_ ⟶ _<_
++-monoʳ-< : LeftMonotonic _<_ _<_ _+_
 +-monoʳ-< r p<q = +-mono-≤-< (≤-refl {r}) p<q
 
 pos+nonNeg⇒pos : ∀ p .{{_ : Positive p}} q .{{_ : NonNegative q}} → Positive (p + q)
@@ -1331,7 +1331,7 @@ module _ where
 *-cancelˡ-≤-pos : ∀ r .{{_ : Positive r}} → r * p ≤ r * q → p ≤ q
 *-cancelˡ-≤-pos {p} {q} r rewrite *-comm r p | *-comm r q = *-cancelʳ-≤-pos r
 
-*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (_* r) Preserves _≤_ ⟶ _≤_
+*-monoʳ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → Monotonic₁ _≤_ _≤_ (_* r)
 *-monoʳ-≤-nonNeg r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin
   toℚᵘ (p * r)        ≃⟨  toℚᵘ-homo-* p r ⟩
   toℚᵘ p ℚᵘ.* toℚᵘ r  ≤⟨  ℚᵘ.*-monoˡ-≤-nonNeg (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩
@@ -1339,10 +1339,10 @@ module _ where
   toℚᵘ (q * r)        ∎)
   where open ℚᵘ.≤-Reasoning
 
-*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → (r *_) Preserves _≤_ ⟶ _≤_
+*-monoˡ-≤-nonNeg : ∀ r .{{_ : NonNegative r}} → Monotonic₁ _≤_ _≤_ (r *_)
 *-monoˡ-≤-nonNeg r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonNeg r
 
-*-monoʳ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (_* r) Preserves _≤_ ⟶ _≥_
+*-monoʳ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → Monotonic₁ _≤_ _≥_ (_* r)
 *-monoʳ-≤-nonPos r {p} {q} p≤q = toℚᵘ-cancel-≤ (begin
   toℚᵘ (q * r)        ≃⟨ toℚᵘ-homo-* q r ⟩
   toℚᵘ q ℚᵘ.* toℚᵘ r  ≤⟨ ℚᵘ.*-monoˡ-≤-nonPos (toℚᵘ r) (toℚᵘ-mono-≤ p≤q) ⟩
@@ -1350,7 +1350,7 @@ module _ where
   toℚᵘ (p * r)        ∎)
   where open ℚᵘ.≤-Reasoning
 
-*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → (r *_) Preserves _≤_ ⟶ _≥_
+*-monoˡ-≤-nonPos : ∀ r .{{_ : NonPositive r}} → Monotonic₁ _≤_ _≥_ (r *_)
 *-monoˡ-≤-nonPos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoʳ-≤-nonPos r
 
 *-cancelʳ-≤-neg : ∀ r .{{_ : Negative r}} → p * r ≤ q * r → p ≥ q
@@ -1395,7 +1395,7 @@ nonPos*nonPos⇒nonPos p q = nonNegative $ begin
 ------------------------------------------------------------------------
 -- Properties of _*_ and _<_
 
-*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → (_* r) Preserves _<_ ⟶ _<_
+*-monoˡ-<-pos : ∀ r .{{_ : Positive r}} → Monotonic₁ _<_ _<_ (_* r)
 *-monoˡ-<-pos r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict
   toℚᵘ (p * r)        ≃⟨ toℚᵘ-homo-* p r ⟩
   toℚᵘ p ℚᵘ.* toℚᵘ r  <⟨ ℚᵘ.*-monoˡ-<-pos (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩
@@ -1403,7 +1403,7 @@ nonPos*nonPos⇒nonPos p q = nonNegative $ begin
   toℚᵘ (q * r)        ∎)
   where open ℚᵘ.≤-Reasoning
 
-*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → (r *_) Preserves _<_ ⟶ _<_
+*-monoʳ-<-pos : ∀ r .{{_ : Positive r}} → Monotonic₁ _<_ _<_ (r *_)
 *-monoʳ-<-pos r {p} {q} rewrite *-comm r p | *-comm r q = *-monoˡ-<-pos r
 
 *-cancelˡ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → r * p < r * q → p < q
@@ -1417,7 +1417,7 @@ nonPos*nonPos⇒nonPos p q = nonNegative $ begin
 *-cancelʳ-<-nonNeg : ∀ r .{{_ : NonNegative r}} → ∀ {p q} → p * r < q * r → p < q
 *-cancelʳ-<-nonNeg r {p} {q} rewrite *-comm p r | *-comm q r = *-cancelˡ-<-nonNeg r
 
-*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → (_* r) Preserves _<_ ⟶ _>_
+*-monoˡ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (_* r)
 *-monoˡ-<-neg r {p} {q} p<q = toℚᵘ-cancel-< (begin-strict
   toℚᵘ (q * r)        ≃⟨ toℚᵘ-homo-* q r ⟩
   toℚᵘ q ℚᵘ.* toℚᵘ r  <⟨ ℚᵘ.*-monoˡ-<-neg (toℚᵘ r) (toℚᵘ-mono-< p<q) ⟩
@@ -1425,7 +1425,7 @@ nonPos*nonPos⇒nonPos p q = nonNegative $ begin
   toℚᵘ (p * r)        ∎)
   where open ℚᵘ.≤-Reasoning
 
-*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → (r *_) Preserves _<_ ⟶ _>_
+*-monoʳ-<-neg : ∀ r .{{_ : Negative r}} → Monotonic₁ _<_ _>_ (r *_)
 *-monoʳ-<-neg r {p} {q} rewrite *-comm r p | *-comm r q = *-monoˡ-<-neg r
 
 *-cancelˡ-<-nonPos : ∀ r .{{_ : NonPositive r}} → r * p < r * q → p > q
@@ -1611,15 +1611,15 @@ open ⊓-⊔-latticeProperties public
 ------------------------------------------------------------------------
 -- Other properties of _⊓_ and _⊔_
 
-mono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q
 mono-≤-distrib-⊔ {f} = ⊓-⊔-properties.mono-≤-distrib-⊔ (cong f)
 
-mono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≤_ →
+mono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≤_ f →
                    ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q
 mono-≤-distrib-⊓ {f} = ⊓-⊔-properties.mono-≤-distrib-⊓ (cong f)
 
-mono-<-distrib-⊓ : ∀ {f} → f Preserves _<_ ⟶ _<_ →
+mono-<-distrib-⊓ : ∀ {f} → Monotonic₁ _<_ _<_ f →
                    ∀ p q → f (p ⊓ q) ≡ f p ⊓ f q
 mono-<-distrib-⊓ {f} f-mono-< p q with <-cmp p q
 ... | tri< p<q p≢r  p≯q = begin
@@ -1638,7 +1638,7 @@ mono-<-distrib-⊓ {f} f-mono-< p q with <-cmp p q
   f p ⊓ f q  ∎
   where open ≡-Reasoning
 
-mono-<-distrib-⊔ : ∀ {f} → f Preserves _<_ ⟶ _<_ →
+mono-<-distrib-⊔ : ∀ {f} → Monotonic₁ _<_ _<_ f →
                    ∀ p q → f (p ⊔ q) ≡ f p ⊔ f q
 mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q
 ... | tri< p<q p≢r  p≯q = begin
@@ -1657,11 +1657,11 @@ mono-<-distrib-⊔ {f} f-mono-< p q with <-cmp p q
   f p ⊔ f q  ∎
   where open ≡-Reasoning
 
-antimono-≤-distrib-⊓ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊓ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ p q → f (p ⊓ q) ≡ f p ⊔ f q
 antimono-≤-distrib-⊓ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊓ (cong f)
 
-antimono-≤-distrib-⊔ : ∀ {f} → f Preserves _≤_ ⟶ _≥_ →
+antimono-≤-distrib-⊔ : ∀ {f} → Monotonic₁ _≤_ _≥_ f →
                        ∀ p q → f (p ⊔ q) ≡ f p ⊓ f q
 antimono-≤-distrib-⊔ {f} = ⊓-⊔-properties.antimono-≤-distrib-⊔ (cong f)
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index ddaeb4e018..924b6faa51 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -37,7 +37,7 @@ open import Relation.Binary.Bundles
 open import Relation.Binary.Structures
   using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
-  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>; Monotonic₁; Monotonic₂)
+  using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>; Monotonic₁; Monotonic₂; LeftMonotonic; RightMonotonic)
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
@@ -858,7 +858,7 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
 ------------------------------------------------------------------------
 -- Properties of _+_ and _<_
 
-+-monoʳ-< : ∀ r → Monotonic₁ _<_ _<_ (r +_)
++-monoʳ-< : LeftMonotonic _<_ _<_ _+_
 +-monoʳ-< r@record{} {p@record{}} {q@record{}} (*<* x<y) = *<* $ begin-strict
   ↥ (r + p) ℤ.* (↧ (r + q))                          ≡⟨ lemma r p q ⟩
   ↥r↧r ℤ.* (↧ p ℤ.* ↧ q) ℤ.+ ↧r↧r ℤ.* (↥ p ℤ.* ↧ q)  <⟨ leq ⟩
@@ -870,7 +870,7 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
     (ℤ.≤-reflexive $ cong (↥r↧r ℤ.*_) (ℤ.*-comm (↧ p) (↧ q)))
     (ℤ.*-monoˡ-<-pos ↧r↧r x<y)
 
-+-monoˡ-< : ∀ r → Monotonic₁ _<_ _<_ (_+ r)
++-monoˡ-< : RightMonotonic _<_ _<_ _+_
 +-monoˡ-< r {p} {q} rewrite +-comm-≡ p r | +-comm-≡ q r = +-monoʳ-< r
 
 +-mono-< : Monotonic₂ _<_ _<_ _<_ _+_

From 87e0cb1432f149232efb2f9d08fd1b35c0b29a90 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 17 Feb 2025 18:52:33 +0000
Subject: [PATCH 16/25] add: missing redefinitions

---
 src/Data/Integer/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 9eaa83c42a..eeecced16d 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -774,7 +774,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
   o ⊖ n         ≡⟨ [1+m]⊖[1+n]≡m⊖n o n ⟨
   suc o ⊖ suc n ∎ where open ≤-Reasoning
 
-⊖-monoʳ->-< : ∀ p → (p ⊖_) Preserves ℕ._>_ ⟶ _<_
+⊖-monoʳ->-< : LeftMonotonic ℕ._>_ _<_ _⊖_
 ⊖-monoʳ->-< zero    {_}     z<s       = -<+
 ⊖-monoʳ->-< zero    {_}     (s<s m<n@(s≤s _)) = -<- m<n
 ⊖-monoʳ->-< (suc p) {suc m} z<s       = begin-strict
@@ -787,7 +787,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
   p ⊖ n         ≡⟨ [1+m]⊖[1+n]≡m⊖n p n ⟨
   suc p ⊖ suc n ∎ where open ≤-Reasoning
 
-⊖-monoˡ-< : ∀ n → (_⊖ n) Preserves ℕ._<_ ⟶ _<_
+⊖-monoˡ-< : RightMonotonic ℕ._<_ _<_ _⊖_
 ⊖-monoˡ-< zero    m<o             = +<+ m<o
 ⊖-monoˡ-< (suc n) {_} {suc o} z<s = begin-strict
   -[1+ n ]      <⟨  -1+m<n⊖m n _ ⟩

From c9e356e7b4bf86822b1e1d0301365b25448071c2 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 17 Feb 2025 19:13:22 +0000
Subject: [PATCH 17/25] refactor: use new lemma

---
 src/Data/Rational/Unnormalised/Properties.agda | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 924b6faa51..6c7783414b 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -828,7 +828,7 @@ private
                       refl (↥ r) (↧ r) (↧ p) (↥ p) (↧ q)
     where open ℤ-solver
 
-+-monoʳ-≤ : ∀ r → Monotonic₁ _≤_ _≤_ (r +_)
++-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
 +-monoʳ-≤ r@record{} {p@record{}} {q@record{}} (*≤* x≤y) = *≤* $ begin
   ↥ (r + p) ℤ.* ↧ (r + q)                                  ≡⟨ lemma r p q ⟩
   r₂ ℤ.* (↧ p ℤ.* ↧ q) ℤ.+ (↧ r ℤ.* ↧ r) ℤ.* (↥ p ℤ.* ↧ q) ≤⟨ leq ⟩
@@ -840,11 +840,12 @@ private
     (ℤ.≤-reflexive $ cong (r₂ ℤ.*_) (ℤ.*-comm (↧ p) (↧ q)))
     (ℤ.*-monoˡ-≤-nonNeg (↧ r ℤ.* ↧ r) x≤y)
 
-+-monoˡ-≤ : ∀ r → Monotonic₁ _≤_ _≤_ (_+ r)
++-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
 +-monoˡ-≤ r {p} {q} rewrite +-comm-≡ p r | +-comm-≡ q r = +-monoʳ-≤ r
 
 +-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
-+-mono-≤ {p} {q} {u} {v} p≤q u≤v = ≤-trans (+-monoˡ-≤ u p≤q) (+-monoʳ-≤ q u≤v)
++-mono-≤ =
+  BC.monoˡ∧monoʳ⇒mono₂ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-trans +-monoʳ-≤ +-monoˡ-≤
 
 p≤q⇒p≤r+q : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
 p≤q⇒p≤r+q {p} {q} r p≤q = subst (_≤ r + q) (+-identityˡ-≡ p) (+-mono-≤ (nonNegative⁻¹ r) p≤q)

From 8528926e8530636ca577543583a6e5da99e4eef0 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Tue, 18 Feb 2025 10:13:33 +0000
Subject: [PATCH 18/25] =?UTF-8?q?refactor:=20one=20more=20use=20of=20`Mono?=
 =?UTF-8?q?tonic=E2=82=81`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Data/Fin/Properties.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e1f2d25d24..5a135726f0 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -902,7 +902,7 @@ pinch-surjective _       zero    = zero , λ { refl → refl }
 pinch-surjective zero    (suc j) = suc (suc j) , λ { refl → refl }
 pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j)
 
-pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
+pinch-mono-≤ : ∀ (i : Fin n) → Monotonic₁ _≤_ _≤_ (pinch i)
 pinch-mono-≤ 0F      {0F}    {k}     0≤n = z≤n
 pinch-mono-≤ 0F      {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k
 pinch-mono-≤ (suc i) {0F}    {k}     0≤n = z≤n

From d3ed088ff6f920171609a022c38a836fddfce309 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 16:37:36 +0000
Subject: [PATCH 19/25] refactor: `Congruent` in terms of `Monotonic`

---
 src/Algebra/Definitions.agda | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index b823ee3e58..eb64aa8e76 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -15,8 +15,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Core using (Rel)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -26,15 +25,18 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
+open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂)
+open import Relation.Nullary.Negation.Core using (¬_)
+
 
 ------------------------------------------------------------------------
 -- Properties of operations
 
 Congruent₁ : Op₁ A → Set _
-Congruent₁ f = f Preserves _≈_ ⟶ _≈_
+Congruent₁ = Monotonic₁ _≈_ _≈_
 
 Congruent₂ : Op₂ A → Set _
-Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
+Congruent₂ = Monotonic₂ _≈_ _≈_ _≈_
 
 LeftCongruent : Op₂ A → Set _
 LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)

From 7fff2769150b4d77c17e5274bbebf62bbb4caa15 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 16:38:19 +0000
Subject: [PATCH 20/25] refactor: de-nest `module Congruence`

---
 CHANGELOG.md                       |  3 ++-
 src/Algebra/Consequences/Base.agda | 31 ++++++++++++++++--------------
 2 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e22b520ec4..2170774f50 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -100,7 +100,8 @@ Additions to existing modules
 
 * In `Algebra.Consequences.Base`:
   ```agda
-  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
+  module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
+  where
     ∙-congˡ : LeftCongruent _≈_ _∙_
     ∙-congʳ : RightCongruent _≈_ _∙_
   ```
diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 570c26eb03..71a49a4f97 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -10,32 +10,35 @@
 module Algebra.Consequences.Base
   {a} {A : Set a} where
 
-open import Algebra.Core
-open import Algebra.Definitions
+open import Algebra.Core using (Op₁; Op₂)
+import Algebra.Definitions as Definitions
 open import Data.Sum.Base
 open import Relation.Binary.Consequences
   using (mono₂⇒monoˡ; mono₂⇒monoʳ)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Definitions using (Reflexive)
+open import Relation.Binary.Definitions
+  using (Reflexive)
 
-module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) where
+module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_)
+                  (cong : Congruent₂ _∙_) (refl : Reflexive _≈_)
+  where
 
-  sel⇒idem : Selective _≈_ _∙_ → Idempotent _≈_ _∙_
-  sel⇒idem sel x = reduce (sel x x)
+  ∙-congˡ : LeftCongruent _∙_
+  ∙-congˡ {x} = mono₂⇒monoˡ {≤₂ = _≈_} {≤₃ = _≈_} (refl {x = x}) cong x
 
-  module Congruence (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) where
+  ∙-congʳ : RightCongruent _∙_
+  ∙-congʳ {x} = mono₂⇒monoʳ {≤₁ = _≈_} {≤₃ = _≈_} (refl {x = x}) cong x
 
-    ∙-congˡ : LeftCongruent _≈_ _∙_
-    ∙-congˡ = mono₂⇒monoˡ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong _
+module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
 
-    ∙-congʳ : RightCongruent _≈_ _∙_
-    ∙-congʳ = mono₂⇒monoʳ {≤₁ = _≈_} {≤₂ = _≈_} {≤₃ = _≈_} refl cong _
+  sel⇒idem : Selective _∙_ → Idempotent _∙_
+  sel⇒idem sel x = reduce (sel x x)
 
-module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
+module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
-                                     SelfInverse _≈_ f →
-                                     Involutive _≈_ f
+                                     SelfInverse f →
+                                     Involutive f
   reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
 ------------------------------------------------------------------------

From 49c08544ee89683f41c928381f937fce3ba03bde Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 19 Feb 2025 16:38:45 +0000
Subject: [PATCH 21/25] fix: tighten `import`s

---
 src/Algebra/Consequences/Propositional.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
index 29490cbd0c..a711853acf 100644
--- a/src/Algebra/Consequences/Propositional.agda
+++ b/src/Algebra/Consequences/Propositional.agda
@@ -20,7 +20,7 @@ open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Relation.Unary using (Pred)
 
-open import Algebra.Core
+open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Definitions {A = A} _≡_
 import Algebra.Consequences.Setoid (setoid A) as Base
 

From 071d50d999c2415faebb35bf7104a1b1db0e33bc Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Mon, 7 Apr 2025 09:56:16 +0100
Subject: [PATCH 22/25] fix: make relation arguments explicit

---
 src/Algebra/Consequences/Base.agda    | 4 ++--
 src/Data/Nat/Properties.agda          | 6 +++---
 src/Relation/Binary/Consequences.agda | 2 +-
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index 71a49a4f97..e4114ba017 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -24,10 +24,10 @@ module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions
   where
 
   ∙-congˡ : LeftCongruent _∙_
-  ∙-congˡ {x} = mono₂⇒monoˡ {≤₂ = _≈_} {≤₃ = _≈_} (refl {x = x}) cong x
+  ∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x
 
   ∙-congʳ : RightCongruent _∙_
-  ∙-congʳ {x} = mono₂⇒monoʳ {≤₁ = _≈_} {≤₃ = _≈_} (refl {x = x}) cong x
+  ∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x
 
 module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
 
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 40512cc4ef..009c1eb179 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -711,10 +711,10 @@ m+n≤o⇒n≤o (suc m) m+n<o = m+n≤o⇒n≤o m (<⇒≤ m+n<o)
 +-mono-≤ {_} {_} (s≤s m≤n) o≤p = s≤s (+-mono-≤ m≤n o≤p)
 
 +-monoˡ-≤ : RightMonotonic _≤_ _≤_ _+_
-+-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl +-mono-≤
++-monoˡ-≤ = mono₂⇒monoʳ _ _ _≤_ ≤-refl +-mono-≤
 
 +-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _+_
-+-monoʳ-≤ = mono₂⇒monoˡ {≤₃ = _≤_} ≤-refl +-mono-≤
++-monoʳ-≤ = mono₂⇒monoˡ _ _ _≤_ ≤-refl +-mono-≤
 
 +-mono-<-≤ : Monotonic₂ _<_ _≤_ _<_ _+_
 +-mono-<-≤ {_} {suc n} z<s               o≤p = s≤s (m≤n⇒m≤o+n n o≤p)
@@ -977,7 +977,7 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
 *-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
-*-monoˡ-≤ = mono₂⇒monoʳ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
+*-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
 
 *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
 *-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
diff --git a/src/Relation/Binary/Consequences.agda b/src/Relation/Binary/Consequences.agda
index bd59bf053f..45a03ebee3 100644
--- a/src/Relation/Binary/Consequences.agda
+++ b/src/Relation/Binary/Consequences.agda
@@ -104,7 +104,7 @@ module _ (≈₁ : Rel A ℓ₁) (≈₂ : Rel B ℓ₂) {≤₁ : Rel A ℓ₃}
     (mono (reflexive x≈y) (reflexive u≈v))
     (mono (reflexive (sym x≈y)) (reflexive (sym u≈v)))
 
-module _ {≤₁ : Rel A ℓ₁} {≤₂ : Rel B ℓ₂} {≤₃ : Rel C ℓ₂} where
+module _ (≤₁ : Rel A ℓ₁) (≤₂ : Rel B ℓ₂) (≤₃ : Rel C ℓ₂) where
 
   mono₂⇒monoˡ : ∀ {f} → Reflexive ≤₁ →
                 Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f

From 2c82f4261af9fa78bb1f15e2a9467c2b30edc186 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 9 Apr 2025 10:49:02 +0100
Subject: [PATCH 23/25] fix: explicit imports

---
 src/Algebra/Consequences/Base.agda | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
index df5d446ecd..5df61df8ee 100644
--- a/src/Algebra/Consequences/Base.agda
+++ b/src/Algebra/Consequences/Base.agda
@@ -12,7 +12,8 @@ module Algebra.Consequences.Base
 
 open import Algebra.Core using (Op₁; Op₂)
 import Algebra.Definitions as Definitions
-  using (Selective; Idempotent; SelfInverse; Involutive)
+  using (Congruent₂; LeftCongruent; RightCongruent
+        ; Selective; Idempotent; SelfInverse; Involutive)
 open import Data.Sum.Base using (_⊎_; reduce)
 open import Relation.Binary.Consequences
   using (mono₂⇒monoˡ; mono₂⇒monoʳ)

From adf424bcea3fad6dda2c55b3abbe8e6b0d21dd18 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 9 Apr 2025 11:04:58 +0100
Subject: [PATCH 24/25] fix: parameterisation of  proofs

---
 src/Data/Nat/Properties.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index 124d2987ba..3198ad7f4d 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -981,10 +981,10 @@ n≢0∧m>1⇒m*n>1 m n rewrite *-comm m n = m≢0∧n>1⇒m*n>1 n m
 *-mono-≤ (s≤s m≤n) u≤v = +-mono-≤ u≤v (*-mono-≤ m≤n u≤v)
 
 *-monoˡ-≤ : RightMonotonic _≤_ _≤_ _*_
-*-monoˡ-≤ = mono₂⇒monoʳ {≤₃ = _≤_} ≤-refl *-mono-≤
+*-monoˡ-≤ = mono₂⇒monoʳ _ _ _≤_ ≤-refl *-mono-≤
 
 *-monoʳ-≤ : LeftMonotonic _≤_ _≤_ _*_
-*-monoʳ-≤ = mono₂⇒monoˡ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-refl *-mono-≤
+*-monoʳ-≤ = mono₂⇒monoˡ _≤_ _≤_ _≤_ ≤-refl *-mono-≤
 
 *-mono-< : Monotonic₂ _<_ _<_ _<_ _*_
 *-mono-< z<s               u<v@(s≤s _) = 0<1+n

From 2601ae5fc0a8d995862df0882493cdc74d6a0344 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Wed, 9 Apr 2025 11:22:28 +0100
Subject: [PATCH 25/25] fix: parameterisation of `mono` proofs

---
 src/Data/Rational/Unnormalised/Properties.agda | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index c1af6d94fb..b6eeb9ee6b 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -55,7 +55,7 @@ open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable
         ; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous
         ; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_
-        ; tri≈; tri<; tri>)
+        ; tri≈; tri<; tri>; Monotonic₁; LeftMonotonic; RightMonotonic; Monotonic₂)
 import Relation.Binary.Consequences as BC
 open import Relation.Binary.PropositionalEquality
 import Relation.Binary.Properties.Poset as PosetProperties
@@ -863,7 +863,7 @@ private
 
 +-mono-≤ : Monotonic₂ _≤_ _≤_ _≤_ _+_
 +-mono-≤ =
-  BC.monoˡ∧monoʳ⇒mono₂ {≤₁ = _≤_} {≤₂ = _≤_} {≤₃ = _≤_} ≤-trans +-monoʳ-≤ +-monoˡ-≤
+  BC.monoˡ∧monoʳ⇒mono₂ _≤_ _≤_ _≤_ ≤-trans +-monoʳ-≤ +-monoˡ-≤
 
 p≤q⇒p≤r+q : ∀ r .{{_ : NonNegative r}} → p ≤ q → p ≤ r + q
 p≤q⇒p≤r+q {p} {q} r p≤q = subst (_≤ r + q) (+-identityˡ-≡ p) (+-mono-≤ (nonNegative⁻¹ r) p≤q)
@@ -881,7 +881,7 @@ p≤p+q p q rewrite +-comm-≡ p q = p≤q+p p q
 +-monoʳ-< r@record{} {p@record{}} {q@record{}} (*<* x<y) = *<* $ begin-strict
   ↥ (r + p) ℤ.* (↧ (r + q))                          ≡⟨ lemma r p q ⟩
   ↥r↧r ℤ.* (↧ p ℤ.* ↧ q) ℤ.+ ↧r↧r ℤ.* (↥ p ℤ.* ↧ q)  <⟨ leq ⟩
-  ↥r↧r ℤ.* (↧ q ℤ.* ↧ p) ℤ.+ ↧r↧r ℤ.* (↥ q ℤ.* ↧ p)  ≡⟨ sym $ lemma r q p ⟩
+  ↥r↧r ℤ.* (↧ q ℤ.* ↧ p) ℤ.+ ↧r↧r ℤ.* (↥ q ℤ.* ↧ p)  ≡⟨ lemma r q p ⟨
   ↥ (r + q) ℤ.* (↧ (r + p))                          ∎
   where
   open ℤ.≤-Reasoning; ↥r↧r = ↥ r ℤ.* ↧ r; ↧r↧r = ↧ r ℤ.* ↧ r