diff --git a/CHANGELOG.md b/CHANGELOG.md
index 80da9ee48e..603bc96ade 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -24,5 +24,10 @@ Deprecated names
 New modules
 -----------
 
+* Properties of `IdempotentCommutativeMonoid`s refactored out from `Algebra.Solver.IdempotentCommutativeMonoid`:
+  ```agda
+  Algebra.Properties.IdempotentCommutativeMonoid
+  ```
+
 Additions to existing modules
 -----------------------------
diff --git a/src/Algebra/Properties/IdempotentCommutativeMonoid.agda b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda
new file mode 100644
index 0000000000..c5fde763fe
--- /dev/null
+++ b/src/Algebra/Properties/IdempotentCommutativeMonoid.agda
@@ -0,0 +1,38 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Some derivable properties
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
+
+module Algebra.Properties.IdempotentCommutativeMonoid
+  {c ℓ} (M : IdempotentCommutativeMonoid c ℓ) where
+
+open IdempotentCommutativeMonoid M
+
+open import Algebra.Consequences.Setoid setoid
+  using (comm∧distrˡ⇒distrʳ; comm∧distrˡ⇒distr)
+open import Algebra.Definitions _≈_
+  using (_DistributesOverˡ_; _DistributesOverʳ_; _DistributesOver_)
+open import Algebra.Properties.CommutativeSemigroup commutativeSemigroup
+  using (interchange)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+
+------------------------------------------------------------------------
+-- Distributivity
+
+∙-distrˡ-∙ : _∙_ DistributesOverˡ _∙_
+∙-distrˡ-∙ a b c = begin
+    a ∙ (b ∙ c)        ≈⟨ ∙-congʳ (idem a) ⟨
+    (a ∙ a) ∙ (b ∙ c)  ≈⟨ interchange _ _ _ _ ⟩
+    (a ∙ b) ∙ (a ∙ c)  ∎
+
+∙-distrʳ-∙ : _∙_ DistributesOverʳ _∙_
+∙-distrʳ-∙ = comm∧distrˡ⇒distrʳ ∙-cong comm ∙-distrˡ-∙
+
+∙-distr-∙ : _∙_ DistributesOver _∙_
+∙-distr-∙ = comm∧distrˡ⇒distr ∙-cong comm ∙-distrˡ-∙