The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 08/09/2016 01:53 PM, Soegtrop, Michael wrote:
> It might help to define the multiply operator as ((a mod m) * (b mod m)) mod 
> m. I think ring simplifies x+x+x+x to 4*x which then should be trivially 
> simplified to 1*x. With the operators defined as is, this is less trivial to 
> see. I ask Valentin to try this.

Not sure it helps. I think the way to go is to follow what Assia 
explained in her message related to boolean ring:

https://sympa.inria.fr/sympa/arc/coq-club/2016-04/msg00059.html

You need the ring to compute with coeffficients in Z/3Z otherwise you 
miss things.

--
Kaurent