[Agda] commutative ring solver

[mechvel at scico.botik.ru]

Can anybody, please, advise on the following subject?
I need to prove in Agda the statements like

    (a b c : Carrier) → (a - b) * c ≈ c * a - c * b

(a bit more complex ones)
in the environment of CommutativeRing.

What is an appropriate kind of a solver in lib-1.3 ?
What to import? How to call?

I attempted with the code like

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

  module _ {α α=} (R : CommutativeRing α α=)
                  (open CommutativeRing R using (Carrier; _≈_; _-_; _*_)
                                          renaming (refl to ≈refl)
                  )
                  (_≟_ : Decidable _≈_)
    where
    module ACRSolver = Solver (ACR.fromCommutativeSemiring R) _≟_
    open ACRSolver

    lemma :  (a b c : Carrier) → (a - b) * c ≈ c * a - c * b
    lemma a b c =
          solve 3 (λ x y z →  (x :- y) :* z := (z :* x) :- (z :* y))
                  ≈refl a b c

And it is not type-checked.

Thanks,

------
Sergei