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: 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


Archive powered by MHonArc 2.6.18.

Top of Page