The Coq mailing list

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

On 08/09/2016 11:23 AM, Soegtrop, Michael wrote:
> Dear Coq Users,
>
> another approach is to show that these modulo operations form a ring and use 
> a rewrite database to transform normal mod expressions into expression using 
> modulo arithmetic operators.

It works but your ring somewhat misses the fact that 3 mod 3 = 0 but
applying it twice makes the trick

Lemma Test1 : forall x : Z,
  (x mod 3)%Z = (((x mod 3 - (- x) mod 3) mod 3 - ((- x) mod 3 - x mod 
3) mod 3) mod 3)%Z.
Proof.
  intros x.
  apply sym_equal.
  rewrite <- (Zmod_mod).
  autorewrite with HdbMod.
ring_simplify.
ring.
Qed.