coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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?, Soegtrop, Michael, 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?, Gaetan Gilbert, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 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?, Laurent Thery, 08/09/2016
- RE: [Coq-Club] how to proof in Z modulo?, Soegtrop, Michael, 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?, Laurent Thery, 08/09/2016
Archive powered by MHonArc 2.6.18.