The Coq mailing list

[Jiten Pathy <jpathy AT fssrv.net>]

Thanks Frederic, i will see, if i can draw any tricks to complete my proof.
Also, thanks Ben for the pointers.

On Thu, Jan 15, 2015 at 10:15 AM, Ben 
<midfield AT gmail.com>
 wrote:
> here are some useful links:
>
> https://sympa.inria.fr/sympa/arc/coq-club/2014-11/msg00124.html
> https://gist.github.com/anonymous/e9493ce195219c4c2b18
>
> i tried to do it myself i failed -- i'm just a beginner.  at some point i 
> convinced myself that the right way to do it is
>
> - prove pigeonhole for lists of nats (using decidable equality)
>
> - convert the general problem into a problem about lists of nats by using 
> indices
>
> but i got bogged down in details.  also there's a Prop vs Type issue with 
> appears_in, i think.
>
> best, ben
>
>> On Jan 15, 2015, at 12:14 AM, Jiten Pathy 
>> <jpathy AT fssrv.net>
>>  wrote:
>>
>> Hello,
>> Trying to prove pigeon hole from SF using excluded_middle. Stuck while
>> doig the following. A hint on what i am doing wrong?
>>
>> https://gist.github.com/anonymous/548325557388612bd60e
>