--- a/src/Gutil.agda	Tue May 31 18:45:43 2022 +0900
+++ b/src/Gutil.agda	Tue Jan 24 16:40:39 2023 +0900
@@ -128,3 +128,17 @@
      (f ∙ g) ⁻¹
      ∎ where open EqReasoning (Algebra.Group.setoid G)
 
+open import Tactic.MonoidSolver using (solve; solve-macro)
+
+lemma7 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
+lemma7 f g = begin
+     g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ε                                ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩
+     g ⁻¹ ∙ f ⁻¹  ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ )         ≈⟨ solve monoid ⟩
+     g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))    ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩
+     g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))                   ≈⟨ solve monoid ⟩
+     (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε)                  ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩
+     (f ∙ g) ⁻¹ ∙ ε                                  ≈⟨ solve monoid ⟩
+     (f ∙ g) ⁻¹
+     ∎ where open EqReasoning (Algebra.Group.setoid G)
+