Improve `Algebra.Solver` documentation

[mechvel]

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.

[MatthewDaggitt]

See Algebra.Solver.CommutativeMonoid.Example.

You're right a README file would be good though.

[mechvel]

Following Algebra.Solver.CommutativeMonoid.Example, I write

lemma b p p' q q' a =      
  let _∙_ = _⊕_
      x   = var 0F
      y   = var (sucF 0F)
      y'  = var (sucF (sucF 0F))
      z   = var (sucF (sucF (sucF 0F)))
      z'  = var (sucF (sucF (sucF (sucF 0F))))
      u   = var (sucF (sucF (sucF (sucF (sucF 0F)))))
  in
  prove 6 (x ∙ ((y ∙ y') ∙ ((z ∙ z') ∙ u))) (y ∙ (z ∙ (y' ∙ (x ∙ (z' ∙ u)))))
              (b ∷ p ∷ p' ∷ q ∷ q' ∷ a ∷ [])

It works, but what can be a nice replacement for repeating sucF (on Fin 6) so many times?
People wrote something about this, but I do not recall.

You're right a README file would be good though.

In this particular case, I wrote to GitHub because I did not see the file name "Example". And to see it one needs to further enter the folder of CommutativeMonoid/. Many people would guess to enter it, but not all of them.

[gallais]

Have you tried using #_?

[mechvel]

I see now. Thank you.
Now, it is

  lemma0 b p p' q q' a =
    let _∙_  = _⊕_;
        x = var (# 0);   y  = var (# 1);   y' = var (# 2)    
        z = var (# 3);   z' = var (# 4);   u  = var (# 5)
    in  
    prove 6 (x ∙ ((y ∙ y') ∙ ((z ∙ z') ∙ u)))  (y ∙ (z ∙ (y' ∙ (x ∙ (z' ∙ u)))))
                (b ∷ p ∷ p' ∷ q ∷ q' ∷ a ∷ [])