coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Clément Pit--Claudel <clement.pit AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] how to proof in Z modulo?
- Date: Tue, 9 Aug 2016 03:32:06 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
- Ironport-phdr: 9a23:2vC86R/ajGc1AP9uRHKM819IXTAuvvDOBiVQ1KB91+scTK2v8tzYMVDF4r011RmSDN2duqsP0rOG+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzS9eZ1p3nn8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT4r9Zf9HFbvOtk/MpdW437eb45RPpWFmcIKWcwsebvNBzOSxe43noAFyA9lhNVDwXBpEXxWpr0vy3m8PJ8xAGVOMT3SfY/XjH0vPQjcwPhlCpSb21xy2rQkMEl1K8=
On 2016-08-09 03:13, Laurent Thery wrote:
> replace 4 with (3 + 1) by lia.
> rewrite Zplus_mod.
> rewrite Z_mod_same_full.
> replace (0 + (1 mod 3)) with (1 mod 3) by lia.
> rewrite Zmod_mod.
> rewrite Zmod_small; lia.
> Qed.
I think this part can be replaced with reflexivity. :)
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] how to proof in Z modulo?, Daniel de Rauglaudre, 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?, Clément Pit--Claudel, 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?, Clément Pit--Claudel, 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?, 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?, Soegtrop, Michael, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Clément Pit--Claudel, 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?, Clément Pit--Claudel, 08/09/2016
- Re: [Coq-Club] how to proof in Z modulo?, Laurent Thery, 08/09/2016
Archive powered by MHonArc 2.6.18.