coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jiten Pathy <jpathy AT fssrv.net>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] pigeon hole principal
- Date: Thu, 15 Jan 2015 00:14:24 -0800
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
- [Coq-Club] pigeon hole principal, Jiten Pathy, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Frédéric Blanqui, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Ben, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, Jiten Pathy, 01/15/2015
- Re: [Coq-Club] pigeon hole principal, gallais, 01/16/2015
- Re: [Coq-Club] pigeon hole principal, Daniel Schepler, 01/16/2015
Archive powered by MHonArc 2.6.18.