[ new ] ⁻¹-anti-homo-(// | \\)

CHANGELOG.md

@@ -213,6 +213,7 @@ 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
   ```
 
 * In `Algebra.Properties.Loop`:

src/Algebra/Properties/Group.agda

@@ -126,6 +126,14 @@ 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 ∎
+
 \\≗flip-//⇒comm : (∀ x y → x \\ y ≈ y // x) → Commutative _∙_
 \\≗flip-//⇒comm \\≗//ᵒ x y = begin
   x ∙ y                ≈⟨ ∙-congˡ (//-rightDividesˡ x y) ⟨