diff --git a/CHANGELOG.md b/CHANGELOG.md
index e159cc52df..f3b5c45659 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -155,6 +155,20 @@ Additions to existing modules
   ⊕-∧-booleanRing   : BooleanRing _ _
   ```
 
+* In `Algebra.Module.Properties.LeftModule`:
+  ```agda
+  -1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m
+  -‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m)
+  -ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m)
+  ```
+
+* In `Algebra.Module.Properties.RightModule`:
+  ```agda
+  -1#*ₗm≈-ᴹm : m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m
+  -‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r)
+  -ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r)
+  ```
+
 * In `Algebra.Properties.RingWithoutOne`:
   ```agda
   [-x][-y]≈xy : ∀ x y → - x * - y ≈ x * y
diff --git a/src/Algebra/Module/Properties/LeftModule.agda b/src/Algebra/Module/Properties/LeftModule.agda
index ad6d33cc67..74cc1d8148 100644
--- a/src/Algebra/Module/Properties/LeftModule.agda
+++ b/src/Algebra/Module/Properties/LeftModule.agda
@@ -23,3 +23,27 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
   renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
            ; inverseʳ-unique to inverseʳ-uniqueᴹ
            ; ⁻¹-involutive to -ᴹ-involutive)
+
+open import Algebra.Properties.Ring ring
+
+open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+
+-‿distrib-*ₗ : ∀ r m → - r *ₗ m ≈ᴹ -ᴹ (r *ₗ m)
+-‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (- r *ₗ m) (begin
+  r *ₗ m +ᴹ - r *ₗ m ≈⟨ *ₗ-distribʳ m r (- r) ⟨
+  (r - r) *ₗ m       ≈⟨ *ₗ-congʳ (-‿inverseʳ r) ⟩
+  0# *ₗ m            ≈⟨ *ₗ-zeroˡ m ⟩
+  0ᴹ                 ∎)
+
+-ᴹ‿distrib-*ₗ : ∀ r m → r *ₗ (-ᴹ m) ≈ᴹ -ᴹ (r *ₗ m)
+-ᴹ‿distrib-*ₗ r m = inverseʳ-uniqueᴹ (r *ₗ m) (r *ₗ (-ᴹ m)) (begin
+    r *ₗ m +ᴹ r *ₗ (-ᴹ m) ≈⟨ *ₗ-distribˡ r m (-ᴹ m) ⟨
+    r *ₗ (m +ᴹ (-ᴹ m))    ≈⟨ *ₗ-congˡ (-ᴹ‿inverseʳ m) ⟩
+    r *ₗ 0ᴹ               ≈⟨ *ₗ-zeroʳ r ⟩
+    0ᴹ                    ∎)
+
+-1#*ₗm≈-ᴹm : ∀ m → - 1# *ₗ m ≈ᴹ -ᴹ m
+-1#*ₗm≈-ᴹm m = begin
+  - 1# *ₗ m    ≈⟨ -‿distrib-*ₗ 1# m ⟩
+  -ᴹ (1# *ₗ m) ≈⟨ -ᴹ‿cong (*ₗ-identityˡ m) ⟩
+  -ᴹ m         ∎
diff --git a/src/Algebra/Module/Properties/RightModule.agda b/src/Algebra/Module/Properties/RightModule.agda
index ef6b7c9f90..2f6deb7c74 100644
--- a/src/Algebra/Module/Properties/RightModule.agda
+++ b/src/Algebra/Module/Properties/RightModule.agda
@@ -23,3 +23,28 @@ open import Algebra.Properties.AbelianGroup +ᴹ-abelianGroup public
   renaming (inverseˡ-unique to inverseˡ-uniqueᴹ
            ; inverseʳ-unique to inverseʳ-uniqueᴹ
            ; ⁻¹-involutive to -ᴹ-involutive)
+
+open import Algebra.Properties.Ring ring
+
+open import Relation.Binary.Reasoning.Setoid ≈ᴹ-setoid
+
+-‿distrib-*ᵣ : ∀ m r → m *ᵣ (- r) ≈ᴹ -ᴹ (m *ᵣ r)
+-‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) (m *ᵣ - r) (begin
+  m *ᵣ r +ᴹ m *ᵣ - r ≈⟨ *ᵣ-distribˡ m r (- r) ⟨
+  m *ᵣ (r - r)       ≈⟨ *ᵣ-congˡ (-‿inverseʳ r) ⟩
+  m *ᵣ 0#            ≈⟨ *ᵣ-zeroʳ m ⟩
+  0ᴹ                 ∎)
+
+-ᴹ‿distrib-*ᵣ : ∀ m r → (-ᴹ m) *ᵣ r ≈ᴹ -ᴹ (m *ᵣ r)
+-ᴹ‿distrib-*ᵣ m r = inverseʳ-uniqueᴹ (m *ᵣ r) ((-ᴹ m) *ᵣ r) (begin
+    m *ᵣ r +ᴹ (-ᴹ m) *ᵣ r ≈⟨ *ᵣ-distribʳ r m (-ᴹ m) ⟨
+    (m +ᴹ -ᴹ m) *ᵣ r      ≈⟨ *ᵣ-congʳ (-ᴹ‿inverseʳ m) ⟩
+    0ᴹ *ᵣ r               ≈⟨ *ᵣ-zeroˡ r ⟩
+    0ᴹ                    ∎)
+
+m*ᵣ-1#≈-ᴹm : ∀ m → m *ᵣ (- 1#) ≈ᴹ -ᴹ m
+m*ᵣ-1#≈-ᴹm m = begin
+  m *ᵣ (- 1#)  ≈⟨ -‿distrib-*ᵣ m 1# ⟩
+  -ᴹ (m *ᵣ 1#) ≈⟨ -ᴹ‿cong (*ᵣ-identityʳ m) ⟩
+  -ᴹ m         ∎
+