coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Laurent Thery <Laurent.Thery AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] how to proof in Z modulo?
- Date: Tue, 9 Aug 2016 14:41:08 +0200
On 08/09/2016 01:43 PM, Soegtrop, Michael wrote:
(not sure why none is required for submod)
you must have proved somewhere in the ring structure that a - b = a + (- b), so minus acts as a derived operator.
- Re: [Coq-Club] how to proof in Z modulo?, (continued)
- 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?, 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?, 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.