Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to proof in Z modulo?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to proof in Z modulo?


Chronological Thread 
  • From: e+coq-club AT x80.org (Emilio Jesús Gallego Arias)
  • To: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] how to proof in Z modulo?
  • Date: Tue, 09 Aug 2016 14:41:06 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e+coq-club AT x80.org; spf=Neutral smtp.mailfrom=e+coq-club AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-b.ensmp.fr
  • Organization: X80 Heavy Industries

Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>
writes:

> 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

Apart from all the useful suggestions already given, working directly in
the 'Z_3 ring could be of help in this case:

From mathcomp Require Import all_ssreflect all_algebra.

Open Scope ring_scope.
Import GRing.Theory.

Lemma U (x : 'Z_3) : x - (- x) - (- x - x) = x.
Proof. by rewrite opprB opprK addrA -mulr2n -mulrSr mulrn_char ?add0r. Qed.

Best,
E.



Archive powered by MHonArc 2.6.18.

Top of Page