coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n.

From: frank maltman <frank.maltman AT googlemail.com>
To: Pierre Casteran <pierre.casteran AT labri.fr>
Cc: <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n.
Date: Sun, 22 May 2011 08:54:12 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:cc:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=FB9dOqzOnBs5mOR2VNdUxZ/3tD3Qc5/y8nZO5bAxF2PtbVupMNtGUWW8EySkh/NU9L y+ZO5iqyqx+8ZwjLKauOP60ZdJ86JsBki+TJdeFs++k2tQ7iy7muRgV1y/b2Icdkh7xF T/Jt01aRHpciYd5mCFfsNYGqFrYWY2CZwSxLE=

On Sun, 22 May 2011 07:50:01 +0200
Pierre Casteran
<pierre.casteran AT labri.fr>
wrote:
>
> Hello Frank,
>
> In that module, there is a lemma that can be used in many situations,
> since it gives you a specification of div2. In combination with even's
> decidability, you can prove a lot of properties.

Hello.

Thanks for the reply. Seems I have a lot of reading to do...

[Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
- Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Chris Dams
  - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
    - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., julien forest
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
      - Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., Pierre Casteran
        
        Re: [Coq-Club] Stuck on a proof of div2 (n + n) = n., frank maltman