[Agda] Solver usage

[Sergei Meshveliani]

Can anybody, please, give a hint on the usage of the Standard Library
Solver ?

For example, consider proving 

    lemma :  (a b : Carrier) → a * b - b * a ≈ 0#

for an arbitrary CommutativeRing.
I try this:

-------------------------------------------------------
open import Relation.Binary using (Decidable)
open import Algebra         using (CommutativeRing)
import Algebra.Solver.Ring.Simple as Solver
import Algebra.Solver.Ring.AlmostCommutativeRing as ACR

module _ {α α=} (R : CommutativeRing α α=)
                (open CommutativeRing R using (_≈_))
                (_≟_ : Decidable _≈_)
  where
  open CommutativeRing R using (Carrier; _-_; _*_; 0#)
                         renaming (refl to ≈refl)

  module ACRSolver = Solver (ACR.fromCommutativeRing R) _≟_
  open ACRSolver

  lemma :  (a b : Carrier) → ((a * b) - (b * a)) ≈ 0#
  lemma a b =
        solve 2 (λ x y →  ((x :* y) :- (y :* x)) := (con 0#))
                a b
                -- ≈refl
-------------------------------------------------------------

And it does not work.
Please, how to fix?

If the solver cannot do this for CommutativeRing, all right, may be it
can solve it for CommutativeSemiring -- for 
                                        (a * b) ≈ (b * a)
?
(for, probably, Semiring has not _-_).

Thanks,

------
Sergei