[Agda] Solver usage

[Sergei Meshveliani]

On Wed, 2019-01-23 at 14:29 +0300, Sergei Meshveliani wrote:

> The question is: 
> how to prove with RingSolver the following three equalities in an 
> arbitrary  CommutativeSemiring: 
> 
>  (I)
>  (((n1 * d2 + n2 * d1) * d3) + n3 * d12) * (d1 * d23)	
>  ≈
>  (n1 * d23 + (n2 * d3 + n3 * d2) * d1) * (d12 * d3)
> 
> [..]


Sorry, I have forgotten to add here:  
                           let d12 = d1 * d2;  d23 = d2 * d3 in ... 

--
SM