diff --git a/CHANGELOG.md b/CHANGELOG.md
index 469c926af8..e29e5aec7b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -196,6 +196,11 @@ Additions to existing modules
     record IsSuccessorSetMonomorphism (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
     record IsSuccessorSetIsomorphism  (⟦_⟧ : N₁.Carrier → N₂.Carrier) : Set _
 
+* In `Algebra.Properties.AbelianGroup`:
+  ```
+  ⁻¹-anti-homo‿- : (x - y) ⁻¹ ≈ y - x
+  ```
+
 * In `Algebra.Properties.Group`:
   ```agda
   isQuasigroup    : IsQuasigroup _∙_ _\\_ _//_
@@ -213,6 +218,8 @@ Additions to existing modules
   ⁻¹-selfInverse  : SelfInverse _⁻¹
   \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
   comm⇒\\≗flip-// : Commutative _∙_ → ∀ x y → x \\ y ≈ y // x
+  ⁻¹-anti-homo-// : (x // y) ⁻¹ ≈ y // x
+  ⁻¹-anti-homo-\\ : (x \\ y) ⁻¹ ≈ y \\ x
   ```
 
 * In `Algebra.Properties.Loop`:
diff --git a/src/Algebra/Properties/AbelianGroup.agda b/src/Algebra/Properties/AbelianGroup.agda
index 87c6b7c6b9..b5eb290081 100644
--- a/src/Algebra/Properties/AbelianGroup.agda
+++ b/src/Algebra/Properties/AbelianGroup.agda
@@ -23,6 +23,9 @@ open import Algebra.Properties.Group group public
 ------------------------------------------------------------------------
 -- Properties of abelian groups
 
+⁻¹-anti-homo‿- : ∀ x y → (x - y) ⁻¹ ≈ y - x
+⁻¹-anti-homo‿- = ⁻¹-anti-homo-//
+
 xyx⁻¹≈y : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
 xyx⁻¹≈y x y = begin
   x ∙ y ∙ x ⁻¹    ≈⟨ ∙-congʳ $ comm _ _ ⟩
diff --git a/src/Algebra/Properties/Group.agda b/src/Algebra/Properties/Group.agda
index 3d4a7d7713..bac2c84d31 100644
--- a/src/Algebra/Properties/Group.agda
+++ b/src/Algebra/Properties/Group.agda
@@ -126,6 +126,22 @@ inverseʳ-unique x y eq = trans (y≈x\\z x y ε eq) (identityʳ _)
   (x ∙ y) ∙ y ⁻¹ ∙ x ⁻¹ ≈⟨ assoc (x ∙ y) (y ⁻¹) (x ⁻¹) ⟩
   x ∙ y ∙ (y ⁻¹ ∙ x ⁻¹) ∎
 
+⁻¹-anti-homo-// : ∀ x y → (x // y) ⁻¹ ≈ y // x
+⁻¹-anti-homo-// x y = begin
+  (x // y) ⁻¹      ≡⟨⟩
+  (x ∙ y ⁻¹) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ x (y ⁻¹) ⟩
+  (y ⁻¹) ⁻¹ ∙ x ⁻¹ ≈⟨ ∙-congʳ (⁻¹-involutive y) ⟩
+  y ∙ x ⁻¹         ≡⟨⟩
+  y // x ∎
+
+⁻¹-anti-homo-\\ : ∀ x y → (x \\ y) ⁻¹ ≈ y \\ x
+⁻¹-anti-homo-\\ x y = begin
+  (x \\ y) ⁻¹      ≡⟨⟩
+  (x ⁻¹ ∙ y) ⁻¹    ≈⟨ ⁻¹-anti-homo-∙ (x ⁻¹) y ⟩
+  y ⁻¹ ∙ (x ⁻¹) ⁻¹ ≈⟨ ∙-congˡ (⁻¹-involutive x) ⟩
+  y ⁻¹ ∙ x         ≡⟨⟩
+  y \\ x ∎
+
 \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
 \\≗flip-//⇒comm \\≗//ᵒ x y = begin
   x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨