Can you, please, demonstrate the usage of Algebra.Solver.CommutativeMonoid ? (of lib-1.3). For example, in proving ``` module _ (cMon : CommutativeMonoid _ _) where open CommutativeMonoid cMon lemma : ∀ a a1 b c c1 d → b ∙ ((a ∙ a1) ∙ ((c ∙ c1) ∙ d)) ≈ a ∙ (c ∙ (a1 ∙ (b ∙ (c1 ∙ d)))) lemma = ? ``` (kind of a brief manual, with examples, is needed on using solvers/provers). Thanks.