------------------------------------------------------------------------
-- The Agda standard library
--
-- Some derivable properties
------------------------------------------------------------------------

open import Algebra

module Algebra.Props.AbelianGroup
         {g₁ g₂} (G : AbelianGroup g₁ g₂) where

import Algebra.Props.Group as GP
open import Data.Product
open import Function
import Relation.Binary.EqReasoning as EqR

open AbelianGroup G
open EqR setoid

open GP group public

private
  lemma : ∀ x y → x ∙ y ∙ x ⁻¹ ≈ y
  lemma x y = begin
    x ∙ y ∙ x ⁻¹    ≈⟨ comm _ _ ⟨ ∙-cong ⟩ refl ⟩
    y ∙ x ∙ x ⁻¹    ≈⟨ assoc _ _ _ ⟩
    y ∙ (x ∙ x ⁻¹)  ≈⟨ refl ⟨ ∙-cong ⟩ proj₂ inverse _ ⟩
    y ∙ ε           ≈⟨ proj₂ identity _ ⟩
    y               ∎

⁻¹-∙-comm : ∀ x y → x ⁻¹ ∙ y ⁻¹ ≈ (x ∙ y) ⁻¹
⁻¹-∙-comm x y = begin
  x ⁻¹ ∙ y ⁻¹                         ≈⟨ comm _ _ ⟩
  y ⁻¹ ∙ x ⁻¹                         ≈⟨ sym $ lem ⟨ ∙-cong ⟩ refl ⟩
  x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹) ∙ x ⁻¹  ≈⟨ lemma _ _ ⟩
  y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹               ≈⟨ lemma _ _ ⟩
  (x ∙ y) ⁻¹                          ∎
  where
  lem = begin
    x ∙ (y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹)  ≈⟨ sym $ assoc _ _ _ ⟩
    x ∙ (y ∙ (x ∙ y) ⁻¹) ∙ y ⁻¹  ≈⟨ sym $ assoc _ _ _ ⟨ ∙-cong ⟩ refl ⟩
    x ∙ y ∙ (x ∙ y) ⁻¹ ∙ y ⁻¹    ≈⟨ proj₂ inverse _ ⟨ ∙-cong ⟩ refl ⟩
    ε ∙ y ⁻¹                     ≈⟨ proj₁ identity _ ⟩
    y ⁻¹                         ∎