coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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.

RE: [Coq-Club] how to proof in Z modulo?, (continued)
- Re: [Coq-Club] how to proof in Z modulo?, Vincent Laporte, 08/09/2016
  - Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Emilio Jesús Gallego Arias, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Daniel de Rauglaudre, 08/09/2016