The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi all,

I am trying to prove
  (x mod 3)%Z =
  (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3) mod 3)%Z

And I suffer a lot. Is there a simple way to do that? Is it false?

After
  rewrite <- Zdiv.Zminus_mod.
  rewrite Z.sub_sub_distr, Z.add_comm.
  do 2 rewrite Z.add_sub_assoc.
  destruct (Z.eq_dec (x mod 3) 0) as [Hx| Hx].
   rewrite Hx.
   apply Zdiv.Z_mod_zero_opp_full in Hx; rewrite Hx.
   reflexivity.

   rewrite Zdiv.Z_mod_nz_opp_full; [ | assumption ].

I am still remaining with
  (x mod 3)%Z = ((x mod 3 + x mod 3 - (3 - x mod 3) - (3 - x mod 3)) mod 3)%Z

I think I can do it, but I am tired... do you have a magic incantation
for all this stuff?

Thanks.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/