diff --git a/src/Data/Digit.agda b/src/Data/Digit.agda
index 49370776da..1fde8d22d4 100644
--- a/src/Data/Digit.agda
+++ b/src/Data/Digit.agda
@@ -9,20 +9,24 @@
 module Data.Digit where
 
 open import Data.Nat.Base
-open import Data.Nat.Properties using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n)
-open import Data.Nat.Solver using (module +-*-Solver)
+  using (ℕ; zero; suc; _<_; _/_; _%_; sz<ss; _+_; _*_; 2+; _≤′_)
+open import Data.Nat.Properties
+  using (_≤?_; _<?_; ≤⇒≤′; module ≤-Reasoning; m≤m+n; +-comm; +-assoc;
+    *-distribˡ-+; *-identityʳ)
 open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ)
 open import Data.Bool.Base using (Bool; true; false)
 open import Data.Char.Base using (Char)
-open import Data.List.Base
+open import Data.List.Base using (List; replicate; [_]; _∷_; [])
 open import Data.Product.Base using (∃; _,_)
 open import Data.Vec.Base as Vec using (Vec; _∷_; [])
-open import Data.Nat.DivMod
+open import Data.Nat.DivMod using (m/n<m; _divMod_; result)
 open import Data.Nat.Induction
+  using (Acc; acc; <-wellFounded-fast; <′-Rec; <′-rec)
+open import Function.Base using (_$_)
 open import Relation.Nullary.Decidable using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; sym; cong)
-open import Function.Base using (_$_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; cong; cong₂; module ≡-Reasoning)
 
 ------------------------------------------------------------------------
 -- Digits
@@ -87,20 +91,32 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
   cons : ∀ {m} (r : Digit base) → Pred m → Pred (toℕ r + m * base)
   cons r (ds , eq) = (r ∷ ds , cong (λ i → toℕ r + i * base) eq)
 
-  open ≤-Reasoning
-  open +-*-Solver
+  lem′ : ∀ x k → x + x + (k + x * k) ≡ k + x * 2+ k
+  lem′ x k = begin
+    x + x + (k + x * k)   ≡⟨ +-assoc (x + x) k _ ⟨
+    x + x + k + x * k     ≡⟨ cong (_+ x * k) (+-comm _ k) ⟩
+    k + (x + x) + x * k   ≡⟨ +-assoc k (x + x) _ ⟩
+    k + ((x + x) + x * k) ≡⟨ cong (k +_) (begin
+      (x + x) + x * k       ≡⟨ +-assoc x x _ ⟩
+      x + (x + x * k)       ≡⟨ cong (x +_) (cong (_+ x * k) (*-identityʳ x)) ⟨
+      x + (x * 1 + x * k)   ≡⟨ cong₂ _+_ (*-identityʳ x) (*-distribˡ-+ x 1 k ) ⟨
+      x * 1 + (x * suc k)   ≡⟨ *-distribˡ-+ x 1 (1 + k) ⟨
+      x * 2+ k              ∎) ⟩
+    k + x * 2+ k          ∎
+    where open ≡-Reasoning
 
   lem : ∀ x k r → 2 + x ≤′ r + (1 + x) * (2 + k)
   lem x k r = ≤⇒≤′ $ begin
-    2 + x
-      ≤⟨ m≤m+n _ _ ⟩
-    2 + x + (x + (1 + x) * k + r)
-      ≡⟨ solve 3 (λ x r k → con 2 :+ x :+ (x :+ (con 1 :+ x) :* k :+ r)
-                              :=
-                            r :+ (con 1 :+ x) :* (con 2 :+ k))
-                 refl x r k ⟩
-    r + (1 + x) * (2 + k)
-      ∎
+    2 + x                             ≤⟨ m≤m+n _ _ ⟩
+    2 + x + (x + (1 + x) * k + r)     ≡⟨ cong ((2 + x) +_) (+-comm _ r) ⟩
+    2 + x + (r + (x + (1 + x) * k))   ≡⟨ +-assoc (2 + x) r _ ⟨
+    2 + x + r + (x + (1 + x) * k)     ≡⟨ cong (_+ (x + (1 + x) * k)) (+-comm (2 + x) r) ⟩
+    r + (2 + x) + (x + (1 + x) * k)   ≡⟨ +-assoc r (2 + x) _ ⟩
+    r + ((2 + x) + (x + (1 + x) * k)) ≡⟨ cong (r +_) (cong 2+ (+-assoc x x _)) ⟨
+    r + (2 + (x + x + (1 + x) * k))   ≡⟨ cong (λ z → r + (2+ z)) (lem′ x k) ⟩
+    r + (2 + (k + x * (2 + k)))       ≡⟨⟩
+    r + (1 + x) * (2 + k)             ∎
+    where open ≤-Reasoning
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index e58797ecd1..6243e016eb 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -6,7 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
+{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
 
 module Data.Fin.Properties where
 
@@ -21,7 +21,6 @@ open import Data.Fin.Patterns
 open import Data.Nat.Base as ℕ
   using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕ
-open import Data.Nat.Solver
 open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
@@ -669,12 +668,14 @@ toℕ-combine {suc m} {n} i@0F j = begin
   n ℕ.* toℕ i ℕ.+ toℕ j      ∎
   where open ≡-Reasoning
 toℕ-combine {suc m} {n} (suc i) j = begin
-  toℕ (combine (suc i) j)        ≡⟨⟩
-  toℕ (n ↑ʳ combine i j)         ≡⟨ toℕ-↑ʳ n (combine i j) ⟩
-  n ℕ.+ toℕ (combine i j)        ≡⟨ cong (n ℕ.+_) (toℕ-combine i j) ⟩
-  n ℕ.+ (n ℕ.* toℕ i ℕ.+ toℕ j)  ≡⟨ solve 3 (λ n i j → n :+ (n :* i :+ j) := n :* (con 1 :+ i) :+ j) refl n (toℕ i) (toℕ j) ⟩
-  n ℕ.* toℕ (suc i) ℕ.+ toℕ j    ∎
-  where open ≡-Reasoning; open +-*-Solver
+  toℕ (combine (suc i) j)            ≡⟨⟩
+  toℕ (n ↑ʳ combine i j)             ≡⟨ toℕ-↑ʳ n (combine i j) ⟩
+  n ℕ.+ toℕ (combine i j)            ≡⟨ cong (n ℕ.+_) (toℕ-combine i j) ⟩
+  n ℕ.+ (n ℕ.* toℕ i ℕ.+ toℕ j)     ≡⟨ ℕ.+-assoc n _ (toℕ j) ⟨
+  n ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j       ≡⟨ cong (λ z → z ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j) (ℕ.*-identityʳ n) ⟨
+  n ℕ.* 1 ℕ.+ n ℕ.* toℕ i ℕ.+ toℕ j ≡⟨ cong (ℕ._+ toℕ j) (ℕ.*-distribˡ-+ n 1 (toℕ i) ) ⟨
+  n ℕ.* toℕ (suc i) ℕ.+ toℕ j       ∎
+  where open ≡-Reasoning
 
 combine-monoˡ-< : ∀ {i j : Fin m} (k l : Fin n) →
                   i < j → combine i k < combine j l
@@ -688,7 +689,7 @@ combine-monoˡ-< {m} {n} {i} {j} k l i<j = begin-strict
   n ℕ.* toℕ j            ≤⟨ ℕ.m≤m+n (n ℕ.* toℕ j) (toℕ l) ⟩
   n ℕ.* toℕ j ℕ.+ toℕ l  ≡⟨ toℕ-combine j l ⟨
   toℕ (combine j l)      ∎
-  where open ℕ.≤-Reasoning; open +-*-Solver
+  where open ℕ.≤-Reasoning
 
 combine-injectiveˡ : ∀ (i : Fin m) (j : Fin n) (k : Fin m) (l : Fin n) →
                      combine i j ≡ combine k l → i ≡ k
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index 842058f62e..61477c9acc 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -16,11 +16,11 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.AbelianGroup
 open import Data.Bool.Base using (T; true; false)
 open import Data.Integer.Base renaming (suc to sucℤ)
+open import Data.Integer.Properties.NatLemmas
 open import Data.Nat.Base as ℕ
   using (ℕ; suc; zero; _∸_; s≤s; z≤n; s<s; z<s; s≤s⁻¹; s<s⁻¹)
   hiding (module ℕ)
 import Data.Nat.Properties as ℕ
-open import Data.Nat.Solver
 open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sign.Base as Sign using (Sign)
@@ -45,7 +45,6 @@ open import Algebra.Consequences.Propositional
 open import Algebra.Structures {A = ℤ} _≡_
 module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_
 module ℕtoℤ = Morphism.Definitions ℕ ℤ _≡_
-open +-*-Solver
 
 private
   variable
@@ -1337,15 +1336,6 @@ pred-mono (+≤+ m≤n)         = ⊖-monoˡ-≤ 1 m≤n
 *-zero : Zero 0ℤ _*_
 *-zero = *-zeroˡ , *-zeroʳ
 
-private
-  lemma : ∀ m n o → o ℕ.+ (n ℕ.+ m ℕ.* suc n) ℕ.* suc o
-                  ≡ o ℕ.+ n ℕ.* suc o ℕ.+ m ℕ.* suc (o ℕ.+ n ℕ.* suc o)
-  lemma =
-    solve 3 (λ m n o → o :+ (n :+ m :* (con 1 :+ n)) :* (con 1 :+ o)
-                    := o :+ n :* (con 1 :+ o) :+
-                       m :* (con 1 :+ (o :+ n :* (con 1 :+ o))))
-            refl
-
 *-assoc : Associative _*_
 *-assoc +0 _ _ = refl
 *-assoc i +0 _ rewrite ℕ.*-zeroʳ ∣ i ∣ = refl
@@ -1354,14 +1344,14 @@ private
   | ℕ.*-zeroʳ ∣ i ∣
   | ℕ.*-zeroʳ ∣ sign i Sign.* sign j ◃ ∣ i ∣ ℕ.* ∣ j ∣ ∣
   = refl
-*-assoc -[1+ m ] -[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
-*-assoc -[1+ m ] +[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
-*-assoc +[1+ m ] +[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
-*-assoc +[1+ m ] -[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (lemma m n o)
-*-assoc -[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc +[1+ m ] -[1+ n ] +[1+ o ] = cong -[1+_] (lemma m n o)
-*-assoc +[1+ m ] +[1+ n ] -[1+ o ] = cong -[1+_] (lemma m n o)
+*-assoc -[1+ m ] -[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc -[1+ m ] +[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc +[1+ m ] +[1+ n ] +[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc +[1+ m ] -[1+ n ] -[1+ o ] = cong (+_ ∘ suc) (inner-assoc m n o)
+*-assoc -[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc +[1+ m ] -[1+ n ] +[1+ o ] = cong -[1+_] (inner-assoc m n o)
+*-assoc +[1+ m ] +[1+ n ] -[1+ o ] = cong -[1+_] (inner-assoc m n o)
 
 private
 
@@ -1400,26 +1390,10 @@ private
   rewrite +-identityʳ y
         | +-identityʳ (sign y Sign.* sign x ◃ ∣ y ∣ ℕ.* ∣ x ∣)
         = refl
-*-distribʳ-+ -[1+ m ] -[1+ n ] -[1+ o ] = cong (+_) $
-  solve 3 (λ m n o → (con 2 :+ n :+ o) :* (con 1 :+ m)
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (con 1 :+ o) :* (con 1 :+ m))
-          refl m n o
-*-distribʳ-+ +[1+ m ] +[1+ n ] +[1+ o ] = cong (+_) $
-  solve 3 (λ m n o → (con 1 :+ n :+ (con 1 :+ o)) :* (con 1 :+ m)
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (con 1 :+ o) :* (con 1 :+ m))
-        refl m n o
-*-distribʳ-+ -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] $
-  solve 3 (λ m n o → m :+ (n :+ (con 1 :+ o)) :* (con 1 :+ m)
-                   := (con 1 :+ n) :* (con 1 :+ m) :+
-                      (m :+ o :* (con 1 :+ m)))
-         refl m n o
-*-distribʳ-+ +[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] $
-  solve 3 (λ m n o → m :+ (con 1 :+ m :+ (n :+ o) :* (con 1 :+ m))
-                  := (con 1 :+ n) :* (con 1 :+ m) :+
-                     (m :+ o :* (con 1 :+ m)))
-         refl m n o
+*-distribʳ-+ -[1+ m ] -[1+ n ] -[1+ o ] = cong (+_) $ assoc₁ m n o
+*-distribʳ-+ +[1+ m ] +[1+ n ] +[1+ o ] = cong +[1+_] $ ℕ.suc-injective (assoc₂ m n o)
+*-distribʳ-+ -[1+ m ] +[1+ n ] +[1+ o ] = cong -[1+_] $ assoc₃ m n o
+*-distribʳ-+ +[1+ m ] -[1+ n ] -[1+ o ] = cong -[1+_] $ assoc₄ m n o
 *-distribʳ-+ -[1+ m ] -[1+ n ] +[1+ o ] = begin
   (suc o ⊖ suc n) * -[1+ m ]                ≡⟨ cong (_* -[1+ m ]) ([1+m]⊖[1+n]≡m⊖n o n) ⟩
   (o ⊖ n) * -[1+ m ]                        ≡⟨ distrib-lemma m n o ⟩
diff --git a/src/Data/Integer/Properties/NatLemmas.agda b/src/Data/Integer/Properties/NatLemmas.agda
new file mode 100644
index 0000000000..5aa44bb889
--- /dev/null
+++ b/src/Data/Integer/Properties/NatLemmas.agda
@@ -0,0 +1,69 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some extra lemmas about natural numbers only needed for
+-- Data.Integer.Properties (for distributivity)
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Data.Integer.Properties.NatLemmas where
+
+open import Data.Nat.Base using (ℕ; _+_; _*_; suc)
+open import Data.Nat.Properties
+  using (*-distribʳ-+; *-assoc; +-assoc; +-comm; +-suc)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; cong; cong₂; sym; module ≡-Reasoning)
+
+open ≡-Reasoning
+
+inner-assoc : ∀ m n o → o + (n + m * suc n) * suc o
+                ≡ o + n * suc o + m * suc (o + n * suc o)
+inner-assoc m n o = begin
+  o + (n + m * suc n) * suc o                ≡⟨ cong (o +_) (begin
+    (n + m * suc n) * suc o             ≡⟨ *-distribʳ-+ (suc o) n (m * suc n) ⟩
+    n * suc o + m * suc n * suc o       ≡⟨ cong (n * suc o +_) (*-assoc m (suc n) (suc o)) ⟩
+    n * suc o + m * suc (o + n * suc o) ∎) ⟩
+  o + (n * suc o + m * suc (o + n * suc o))  ≡⟨ +-assoc o _ _ ⟨
+  o + n * suc o + m * suc (o + n * suc o)    ∎
+
+private
+  assoc-comm : ∀ a b c d → a + b + c + d ≡ (a + c) + (b + d)
+  assoc-comm a b c d = begin
+    a + b + c + d     ≡⟨ cong (_+ d) (+-assoc a b c) ⟩
+    a + (b + c) + d   ≡⟨ cong (λ z → a + z + d) (+-comm b c) ⟩
+    a + (c + b) + d   ≡⟨ cong (_+ d) (+-assoc a c b) ⟨
+    (a + c) + b + d   ≡⟨ +-assoc (a + c) b d ⟩
+    (a + c) + (b + d) ∎
+
+  assoc-comm′ : ∀ a b c d → a + (b + (c + d)) ≡ a + c + (b + d)
+  assoc-comm′ a b c d = begin
+    a + (b + (c + d)) ≡⟨ cong (a +_) (+-assoc b c d) ⟨
+    a + (b + c + d)   ≡⟨ cong (λ z → a + (z + d)) (+-comm b c) ⟩
+    a + (c + b + d)   ≡⟨ cong (a +_) (+-assoc c b d) ⟩
+    a + (c + (b + d)) ≡⟨ +-assoc a c _ ⟨
+    a + c + (b + d)   ∎
+
+assoc₁ : ∀ m n o → (2 + n + o) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)
+assoc₁ m n o = begin
+  (2 + n + o) * (1 + m)                  ≡⟨ cong (_* (1 + m)) (assoc-comm 1 1 n o) ⟩
+  ((1 + n) + (1 + o)) * (1 + m)          ≡⟨ *-distribʳ-+ (1 + m) (1 + n) (1 + o) ⟩
+  (1 + n) * (1 + m) + (1 + o) * (1 + m)   ∎
+
+assoc₂ : ∀ m n o → (1 + n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (1 + o) * (1 + m)
+assoc₂ m n o = *-distribʳ-+ (1 + m) (1 + n) (1 + o)
+
+assoc₃ : ∀ m n o → m + (n + (1 + o)) * (1 + m) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))
+assoc₃ m n o = begin
+  m + (n + (1 + o)) * (1 + m)           ≡⟨ cong (m +_) (*-distribʳ-+ (1 + m) n (1 + o)) ⟩
+  m + (n * (1 + m) + (1 + o) * (1 + m)) ≡⟨ +-assoc m _ _ ⟨
+  (m + n * (1 + m)) + (1 + o) * (1 + m) ≡⟨ +-suc _ _ ⟩
+  (1 + n) * (1 + m) + (m + o * (1 + m)) ∎
+
+assoc₄ : ∀ m n o → m + (1 + m + (n + o) * (1 + m)) ≡ (1 + n) * (1 + m) + (m + o * (1 + m))
+assoc₄ m n o = begin
+  m + (1 + m + (n + o) * (1 + m))           ≡⟨ +-suc _ _ ⟩
+  1 + m + (m + (n + o) * (1 + m))           ≡⟨ cong (λ z → suc (m + (m + z))) (*-distribʳ-+ (suc m) n o) ⟩
+  1 + m + (m + (n * (1 + m) + o * (1 + m))) ≡⟨ cong suc (assoc-comm′ m m _ _) ⟩
+  (1 + n) * (1 + m) + (m + o * (1 + m))     ∎
diff --git a/src/Data/Nat/GCD/Lemmas.agda b/src/Data/Nat/GCD/Lemmas.agda
index 3f9a4b6d42..21788f0d88 100644
--- a/src/Data/Nat/GCD/Lemmas.agda
+++ b/src/Data/Nat/GCD/Lemmas.agda
@@ -10,21 +10,23 @@ module Data.Nat.GCD.Lemmas where
 
 open import Data.Nat.Base
 open import Data.Nat.Properties
-open import Data.Nat.Solver
 open import Function.Base using (_$_)
 open import Relation.Binary.PropositionalEquality
 
-open +-*-Solver
 open ≡-Reasoning
 
 private
-  distrib-comm : ∀ x k n → x * k + x * n ≡ x * (n + k)
-  distrib-comm =
-    solve 3 (λ x k n → x :* k :+ x :* n  :=  x :* (n :+ k)) refl
+  comm-factor : ∀ x k n → x * k + x * n ≡ x * (n + k)
+  comm-factor x k n = begin
+    x * k + x * n ≡⟨ +-comm (x * k) _ ⟩
+    x * n + x * k ≡⟨ *-distribˡ-+ x n k ⟨
+    x * (n + k)   ∎
 
   distrib-comm₂ : ∀ d x k n → d + x * (n + k) ≡ d + x * k + x * n
-  distrib-comm₂ =
-    solve 4 (λ d x k n → d :+ x :* (n :+ k) :=  d :+ x :* k :+ x :* n) refl
+  distrib-comm₂ d x k n = begin
+    d + x * (n + k)     ≡⟨ cong (d +_) (comm-factor x k n) ⟨
+    d + (x * k + x * n) ≡⟨ +-assoc d _ _ ⟨
+    d + x * k + x * n   ∎
 
 -- Other properties
 -- TODO: Can this proof be simplified? An automatic solver which can
@@ -40,26 +42,112 @@ lem₀ i j m n eq = begin
 lem₁ : ∀ i j → 2 + i ≤′ 2 + j + i
 lem₁ i j = ≤⇒≤′ $ s≤s $ s≤s $ m≤n+m i j
 
+private
+  times2 : ∀ x → x + x ≡ 2 * x
+  times2 x = cong (x +_) (sym (+-identityʳ x))
+
+  times2′ : ∀ x y → x * y + x * y ≡ 2 * x * y
+  times2′ x y = begin
+    x * y + x * y ≡⟨ times2 (x * y) ⟩
+    2 * (x * y)   ≡⟨ *-assoc 2 x y ⟨
+    2 * x * y     ∎
+
 lem₂ : ∀ d x {k n} →
        d + x * k ≡ x * n → d + x * (n + k) ≡ 2 * x * n
 lem₂ d x {k} {n} eq = begin
   d + x * (n + k)    ≡⟨ distrib-comm₂ d x k n ⟩
-  d + x * k + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
-  x * n + x * n      ≡⟨ solve 3 (λ x n k → x :* n :+ x :* n
-                                       :=  con 2 :* x :* n)
-                                 refl x n k ⟩
+  d + x * k + x * n  ≡⟨ cong (_+ x * n) eq ⟩
+  x * n + x * n      ≡⟨ times2′ x n ⟩
   2 * x * n          ∎
 
+private
+  distrib₃ : ∀ a b c x → (a + b + c) * x ≡ a * x + b * x + c * x
+  distrib₃ a b c x = begin
+    (a + b + c) * x       ≡⟨ *-distribʳ-+ x (a + b) c ⟩
+    (a + b) * x + c * x   ≡⟨ cong (_+ c * x) (*-distribʳ-+ x a b) ⟩
+    a * x + b * x + c * x ∎
+
+  lem₃₁ : ∀ a b c → a + (b + c) ≡ b + a + c
+  lem₃₁ a b c = begin
+    a + (b + c) ≡⟨ +-assoc a b c ⟨
+    (a + b) + c ≡⟨ cong (_+ c) (+-comm a b) ⟩
+    b + a + c   ∎
+
+  +-assoc-comm : ∀ a b c d → a + (b + c + d) ≡ (a + c) + (b + d)
+  +-assoc-comm a b c d = begin
+    a + (b + c + d)   ≡⟨ cong (a +_) (cong (_+ d) (+-comm b c)) ⟩
+    a + (c + b + d)   ≡⟨ cong (a +_) (+-assoc c b d) ⟩
+    a + (c + (b + d)) ≡⟨ +-assoc a c _ ⟨
+    (a + c) + (b + d) ∎
+
+  *-on-right : ∀ a b c {d} → b * c ≡ d → a * b * c ≡ a * d
+  *-on-right a b c {d} eq = begin
+    a * b * c   ≡⟨ *-assoc a b c ⟩
+    a * (b * c) ≡⟨ cong (a *_) eq ⟩
+    a * d       ∎
+
+  *-on-left : ∀ a b c {d} → a * b ≡ d → a * (b * c) ≡ d * c
+  *-on-left a b c {d} eq = begin
+    a * (b * c) ≡⟨ *-assoc a b c ⟨
+    a * b * c   ≡⟨ cong (_* c) eq ⟩
+    d * c       ∎
+
+  +-on-right : ∀ a b c {d} → b + c ≡ d → a + b + c ≡ a + d
+  +-on-right a b c {d} eq = begin
+    a + b + c   ≡⟨ +-assoc a b c ⟩
+    a + (b + c) ≡⟨ cong (a +_) eq ⟩
+    a + d       ∎
+
+  +-on-left : ∀ a b c d → a + b ≡ d → a + (b + c) ≡ d + c
+  +-on-left a b c d eq = begin
+    a + (b + c) ≡⟨ +-assoc a b c ⟨
+    a + b + c   ≡⟨ cong (_+ c) eq ⟩
+    d + c       ∎
+
+  +-focus-mid : ∀ a b c d → a + b + c + d ≡ a + (b + c) + d
+  +-focus-mid a b c d = begin
+    a + b + c + d     ≡⟨ cong (_+ d) (+-assoc a b c) ⟩
+    a + (b + c) + d   ∎
+
+  +-assoc-comm′ : ∀ a b c d → a + b + c + d ≡ a + (b + d) + c
+  +-assoc-comm′ a b c d = begin
+    a + b + c + d     ≡⟨ +-on-left a (b + c) d (a + b + c) (sym $ +-assoc a b c) ⟨
+    a + (b + c + d)   ≡⟨ cong (a +_) (+-on-right b c d (+-comm c d)) ⟩
+    a + (b + (d + c)) ≡⟨ cong (a +_) (+-assoc b d c) ⟨
+    a + (b + d + c)   ≡⟨ +-assoc a _ c ⟨
+    a + (b + d) + c   ∎
+
+  lem₃₂ : ∀ a b c n → a * n + (b * n + a * n + c * n) ≡ (a + a + (b + c)) * n
+  lem₃₂ a b c n = begin
+    a * n + (b * n + a * n + c * n) ≡⟨ cong (a * n +_) (distrib₃ b a c n) ⟨
+    a * n + (b + a + c) * n         ≡⟨ *-distribʳ-+ n a _ ⟨
+    (a + (b + a + c)) * n           ≡⟨ cong (_* n) (+-assoc-comm a b a c) ⟩
+    (a + a + (b + c)) * n           ∎
+
+  mid-to-right : ∀ a b c → a + 2 * b + c ≡ (a + b + c) + b
+  mid-to-right a b c = begin
+    a + 2 * b + c   ≡⟨ cong (λ x → a + x + c) (times2 b) ⟨
+    a + (b + b) + c ≡⟨ +-assoc-comm′ a b c b ⟨
+    a + b + c + b   ∎
+
+  mid-to-left : ∀ a b c → a + 2 * b + c ≡ b + (a + b + c)
+  mid-to-left a b c = begin
+    a + 2 * b + c   ≡⟨ cong (λ x → a + x + c) (times2 b) ⟨
+    a + (b + b) + c ≡⟨ cong (_+ c) (+-on-left a b b _ (+-comm a b)) ⟩
+    b + a + b + c   ≡⟨ +-on-left b (a + b) c (b + a + b) (sym $ +-assoc b a b) ⟨
+    b + (a + b + c) ∎
+
 lem₃ : ∀ d x {i k n} →
        d + (1 + x + i) * k ≡ x * n →
        d + (1 + x + i) * (n + k) ≡ (1 + 2 * x + i) * n
 lem₃ d x {i} {k} {n} eq = begin
-  d + y * (n + k)      ≡⟨ distrib-comm₂ d y k n ⟩
-  d + y * k + y * n    ≡⟨ cong₂ _+_ eq refl ⟩
-  x * n + y * n        ≡⟨ solve 3 (λ x n i → x :* n :+ (con 1 :+ x :+ i) :* n
-                                         :=  (con 1 :+ con 2 :* x :+ i) :* n)
-                                  refl x n i ⟩
-  (1 + 2 * x + i) * n  ∎
+  d + y * (n + k)                     ≡⟨ distrib-comm₂ d y k n ⟩
+  d + y * k + y * n                   ≡⟨ cong (_+ y * n) eq ⟩
+  x * n + y * n                       ≡⟨ cong (x * n +_) (distrib₃ 1 x i n) ⟩
+  x * n + (1 * n + x * n + i * n)     ≡⟨ lem₃₂ x 1 i n  ⟩
+  (x + x + (1 + i)) * n               ≡⟨ cong (_* n) (cong (_+ (1 + i)) (times2 x)) ⟩
+  (2 * x + (1 + i)) * n               ≡⟨ cong (_* n) (lem₃₁ (2 * x) 1 i) ⟩
+  (1 + 2 * x + i) * n                 ∎
   where y = 1 + x + i
 
 lem₄ : ∀ d y {k i} n →
@@ -67,32 +155,29 @@ lem₄ : ∀ d y {k i} n →
        d + y * (n + k) ≡ (1 + 2 * y + i) * n
 lem₄ d y {k} {i} n eq = begin
   d + y * (n + k)          ≡⟨ distrib-comm₂ d y k n ⟩
-  d + y * k + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
-  (1 + y + i) * n + y * n  ≡⟨ solve 3 (λ y i n → (con 1 :+ y :+ i) :* n :+ y :* n
-                                             :=  (con 1 :+ con 2 :* y :+ i) :* n)
-                                      refl y i n ⟩
+  d + y * k + y * n        ≡⟨ cong (_+ y * n) eq ⟩
+  (1 + y + i) * n + y * n  ≡⟨ *-distribʳ-+ n (1 + y + i) y ⟨
+  (1 + y + i + y) * n      ≡⟨ cong (_* n) (mid-to-right 1 y i) ⟨
   (1 + 2 * y + i) * n      ∎
 
 lem₅ : ∀ d x {n k} →
        d + x * n ≡ x * k →
        d + 2 * x * n ≡ x * (n + k)
 lem₅ d x {n} {k} eq = begin
-  d + 2 * x * n      ≡⟨ solve 3 (λ d x n → d :+ con 2 :* x :* n
-                                       :=  d :+ x :* n :+ x :* n)
-                                refl d x n ⟩
-  d + x * n + x * n  ≡⟨ cong₂ _+_ eq refl ⟩
-  x * k + x * n      ≡⟨ distrib-comm x k n ⟩
-  x * (n + k)        ∎
+  d + 2 * x * n       ≡⟨ cong (d +_) (times2′ x n) ⟨
+  d + (x * n + x * n) ≡⟨ +-assoc d (x * n) _ ⟨
+  d + x * n + x * n   ≡⟨ cong (_+ x * n) eq ⟩
+  x * k + x * n       ≡⟨ comm-factor x k n ⟩
+  x * (n + k)         ∎
 
 lem₆ : ∀ d x {n i k} →
        d + x * n ≡ (1 + x + i) * k →
        d + (1 + 2 * x + i) * n ≡ (1 + x + i) * (n + k)
 lem₆ d x {n} {i} {k} eq = begin
-  d + (1 + 2 * x + i) * n  ≡⟨ solve 4 (λ d x i n → d :+ (con 1 :+ con 2 :* x :+ i) :* n
-                                               :=  d :+ x :* n :+ (con 1 :+ x :+ i) :* n)
-                                      refl d x i n ⟩
-  d + x * n + y * n        ≡⟨ cong₂ _+_ eq refl ⟩
-  y * k + y * n            ≡⟨ distrib-comm y k n ⟩
+  d + (1 + 2 * x + i) * n  ≡⟨ cong (λ z → d + z * n) (mid-to-left 1 x i) ⟩
+  d + (x + y) * n          ≡⟨ cong (d +_) (*-distribʳ-+ n x y) ⟩
+  d + (x * n + y * n)      ≡⟨ +-on-left d _ _ _ eq ⟩
+  y * k + y * n            ≡⟨ comm-factor y k n ⟩
   y * (n + k)              ∎
   where y = 1 + x + i
 
@@ -100,12 +185,11 @@ lem₇ : ∀ d y {i} n {k} →
        d + (1 + y + i) * n ≡ y * k →
        d + (1 + 2 * y + i) * n ≡ y * (n + k)
 lem₇ d y {i} n {k} eq = begin
-  d + (1 + 2 * y + i) * n      ≡⟨ solve 4 (λ d y i n → d :+ (con 1 :+ con 2 :* y :+ i) :* n
-                                                   :=  d :+ (con 1 :+ y :+ i) :* n :+ y :* n)
-                                          refl d y i n ⟩
-  d + (1 + y + i) * n + y * n  ≡⟨ cong₂ _+_ eq refl ⟩
-  y * k + y * n                ≡⟨ distrib-comm y k n ⟩
-  y * (n + k)                  ∎
+  d + (1 + 2 * y + i) * n       ≡⟨ cong (λ z → d + z * n) (mid-to-right 1 y i) ⟩
+  d + (1 + y + i + y) * n       ≡⟨ cong (d +_) (*-distribʳ-+ n (1 + y + i) y) ⟩
+  d + ((1 + y + i) * n + y * n) ≡⟨ +-on-left d _ _ _ eq ⟩
+  y * k + y * n                 ≡⟨ comm-factor y k n ⟩
+  y * (n + k)                   ∎
 
 lem₈ : ∀ {i j k q} x y →
        1 + y * j ≡ x * i → j * k ≡ q * i →
@@ -114,17 +198,12 @@ lem₈ {i} {j} {k} {q} x y eq eq′ =
   sym (lem₀ (x * k) (y * q) i k lemma)
   where
   lemma = begin
-    x * k * i        ≡⟨ solve 3 (λ x k i → x :* k :* i
-                                       :=  x :* i :* k)
-                                refl x k i ⟩
-    x * i * k        ≡⟨ cong (_* k) (sym eq) ⟩
-    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
-                                       :=  y :* (j :* k) :+ k)
-                                refl y j k ⟩
+    x * k * i        ≡⟨ *-on-right x k i (*-comm k i) ⟩
+    x * (i * k)      ≡⟨ *-on-left x i k (sym eq) ⟩
+    (1 + y * j) * k  ≡⟨ +-comm k _ ⟩
+    (y * j) * k + k  ≡⟨ cong (_+ k) (*-assoc y j k) ⟩
     y * (j * k) + k  ≡⟨ cong (λ n → y * n + k) eq′ ⟩
-    y * (q * i) + k  ≡⟨ solve 4 (λ y q i k → y :* (q :* i) :+ k
-                                         :=  y :*  q :* i  :+ k)
-                                refl y q i k ⟩
+    y * (q * i) + k  ≡⟨ cong (_+ k) (*-assoc y q i)  ⟨
     y *  q * i  + k  ∎
 
 lem₉ : ∀ {i j k q} x y →
@@ -133,15 +212,19 @@ lem₉ : ∀ {i j k q} x y →
 lem₉ {i} {j} {k} {q} x y eq eq′ =
   sym (lem₀ (y * q) (x * k) i k lemma)
   where
-  lem   = solve 3 (λ a b c → a :* b :* c  :=  b :* c :* a) refl
+  lem : ∀ a b c → a * b * c ≡ b * c * a
+  lem a b c = begin
+    a * b * c   ≡⟨ *-assoc a b c ⟩
+    a * (b * c) ≡⟨ *-comm a _ ⟩
+    b * c * a   ∎
   lemma = begin
     y * q * i        ≡⟨ lem y q i ⟩
-    q * i * y        ≡⟨ cong (λ n → n * y) (sym eq′) ⟩
-    j * k * y        ≡⟨ sym (lem y j k) ⟩
-    y * j * k        ≡⟨ cong (λ n → n * k) (sym eq) ⟩
-    (1 + x * i) * k  ≡⟨ solve 3 (λ x i k → (con 1 :+ x :* i) :* k
-                                       :=  x :* k :* i :+ k)
-                                refl x i k ⟩
+    q * i * y        ≡⟨ cong (λ n → n * y) eq′ ⟨
+    j * k * y        ≡⟨ lem y j k ⟨
+    y * j * k        ≡⟨ cong (λ n → n * k) eq ⟨
+    (1 + x * i) * k  ≡⟨ +-comm k _ ⟩
+    x * i * k + k    ≡⟨ cong (_+ k) (*-on-right x i k (*-comm i k)) ⟩
+    x * (k * i) + k  ≡⟨ cong (_+ k) (*-assoc x k i) ⟨
     x * k * i + k    ∎
 
 lem₁₀ : ∀ {a′} b c {d} e f → let a = suc a′ in
@@ -151,28 +234,29 @@ lem₁₀ {a′} b c {d} e f eq =
   m*n≡1⇒n≡1 (e * f ∸ b * c) d
     (lem₀ (e * f) (b * c) d 1
        (*-cancelʳ-≡ (e * f * d) (b * c * d + 1) _ (begin
-          e * f * d * a        ≡⟨ solve 4 (λ e f d a → e :* f :* d :* a
-                                                   :=  e :* (f :* d :* a))
-                                          refl e f d a ⟩
-          e * (f * d * a)      ≡⟨ sym eq ⟩
-          a + b * (c * d * a)  ≡⟨ solve 4 (λ a b c d → a :+ b :* (c :* d :* a)
-                                                   :=  (b :* c :* d :+ con 1) :* a)
-                                          refl a b c d ⟩
-          (b * c * d + 1) * a  ∎)))
+          e * f * d * a           ≡⟨ *-assoc₄₃ e f d a ⟩
+          e * (f * d * a)         ≡⟨ eq ⟨
+          a + b * (c * d * a)     ≡⟨ cong (a +_) (*-assoc₄₃ b c d a) ⟨
+          a + b * c * d * a       ≡⟨ +-comm a _ ⟩
+          b * c * d * a + a       ≡⟨ cong (b * c * d * a +_) (+-identityʳ a) ⟨
+          b * c * d * a + (a + 0) ≡⟨ *-distribʳ-+ a (b * c * d) 1 ⟨
+          (b * c * d + 1) * a     ∎)))
   where a = suc a′
+        *-assoc₄₃ : ∀ w x y z → w * x * y * z ≡ w * (x * y * z)
+        *-assoc₄₃ w x y z = begin
+          w * x * y * z   ≡⟨ cong (_* z) (*-assoc w x y) ⟩
+          w * (x * y) * z ≡⟨ *-assoc w _ z ⟩
+          w * (x * y * z) ∎
 
 lem₁₁ : ∀ {i j m n k d} x y →
        1 + y * j ≡ x * i → i * k ≡ m * d → j * k ≡ n * d →
        k ≡ (x * m ∸ y * n) * d
 lem₁₁ {i} {j} {m} {n} {k} {d} x y eq eq₁ eq₂ =
   sym (lem₀ (x * m) (y * n) d k (begin
-    x * m * d        ≡⟨ *-assoc x m d ⟩
-    x * (m * d)      ≡⟨ cong (x *_) (sym eq₁) ⟩
-    x * (i * k)      ≡⟨ sym (*-assoc x i k) ⟩
-    x * i * k        ≡⟨ cong₂ _*_ (sym eq) refl ⟩
-    (1 + y * j) * k  ≡⟨ solve 3 (λ y j k → (con 1 :+ y :* j) :* k
-                                       :=  y :* (j :* k) :+ k)
-                                refl y j k ⟩
+    x * m * d        ≡⟨ *-on-right x m d (sym eq₁) ⟩
+    x * (i * k)      ≡⟨ *-on-left x i k (sym eq) ⟩
+    (1 + y * j) * k  ≡⟨ +-comm k _ ⟩
+    y * j * k + k    ≡⟨ cong (_+ k) (*-assoc y j k) ⟩
     y * (j * k) + k  ≡⟨ cong (λ p → y * p + k) eq₂ ⟩
-    y * (n * d) + k  ≡⟨ cong₂ _+_ (sym $ *-assoc y n d) refl ⟩
+    y * (n * d) + k  ≡⟨ cong (_+ k) (*-assoc y n d) ⟨
     y * n * d + k    ∎))
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index 2174d29c74..181e4a6189 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -20,7 +20,6 @@ import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 open import Data.Bool.Base using (T; true; false)
 open import Data.Nat.Base as ℕ using (suc; pred)
 import Data.Nat.Properties as ℕ
-open import Data.Nat.Solver renaming (module +-*-Solver to ℕ-solver)
 open import Data.Integer.Base as ℤ using (ℤ; +0; +[1+_]; -[1+_]; 0ℤ; 1ℤ; -1ℤ)
 open import Data.Integer.Solver renaming (module +-*-Solver to ℤ-solver)
 import Data.Integer.Properties as ℤ
@@ -1123,12 +1122,14 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-inverseˡ p@(mkℚᵘ -[1+ n ] d) = *-inverseˡ (mkℚᵘ +[1+ n ] d)
 *-inverseˡ p@(mkℚᵘ +[1+ n ] d) = *≡* $ cong +[1+_] $ begin
   (n ℕ.+ d ℕ.* suc n) ℕ.* 1 ≡⟨ ℕ.*-identityʳ _ ⟩
-  (n ℕ.+ d ℕ.* suc n)       ≡⟨ cong (n ℕ.+_) (ℕ.*-suc d n) ⟩
-  (n ℕ.+ (d ℕ.+ d ℕ.* n))   ≡⟨ solve 2 (λ n d → n :+ (d :+ d :* n) := d :+ (n :+ n :* d)) refl n d ⟩
-  (d ℕ.+ (n ℕ.+ n ℕ.* d))   ≡⟨ cong (d ℕ.+_) (sym (ℕ.*-suc n d)) ⟩
+  n ℕ.+ d ℕ.* suc n         ≡⟨ cong (n ℕ.+_) (ℕ.*-suc d n) ⟩
+  n ℕ.+ (d ℕ.+ d ℕ.* n)     ≡⟨ trans (sym $ ℕ.+-assoc n d _) (trans
+                                      (cong₂ ℕ._+_ (ℕ.+-comm n d) (ℕ.*-comm d n))
+                                      (ℕ.+-assoc d n _)) ⟩
+  d ℕ.+ (n ℕ.+ n ℕ.* d)     ≡⟨ cong (d ℕ.+_) (sym (ℕ.*-suc n d)) ⟩
   d ℕ.+ n ℕ.* suc d         ≡⟨ ℕ.+-identityʳ _ ⟨
   d ℕ.+ n ℕ.* suc d ℕ.+ 0   ∎
-  where open ≡-Reasoning; open ℕ-solver
+  where open ≡-Reasoning
 
 *-inverseʳ : ∀ p .{{_ : NonZero p}} → p * 1/ p ≃ 1ℚᵘ
 *-inverseʳ p = ≃-trans (*-comm p (1/ p)) (*-inverseˡ p)