coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] 1 < two_power_pos p

From: frank maltman <frank.maltman AT googlemail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] 1 < two_power_pos p
Date: Wed, 8 Jun 2011 23:50:56 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:x-mailer:mime-version:content-type :content-transfer-encoding; b=TblbGXgCW9TIfUxPxpw7WKdESRsiMpXxVyIgN27msThPab0+aXHGOotXy4UmSfobrO JV14iFsTiXW55CTE4fgnZ2zJj0OeJqt+xaXjrbiYM11nHfwTEXdMnCXNaLJvlA1IhZof 4hmBONXisFr2cgJgBU78FuswUuTBuy3r5T2gk=

Hello.

Does anyone have a proof of 1 < two_power_pos p?

It seems quite obviously true given:

Coq < Eval cbv in two_power_pos 0.
Error: Only strictly positive numbers in type "positive".

Coq < Eval cbv in two_power_pos 1.
= 2
: Z

[Coq-Club] 1 < two_power_pos p, frank maltman
- [Coq-Club] Re: 1 < two_power_pos p, frank maltman