coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: 1 < two_power_pos p

From: frank maltman <frank.maltman AT googlemail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Re: 1 < two_power_pos p
Date: Fri, 10 Jun 2011 10:47:14 +0000
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=date:from:to:subject:message-id:in-reply-to:references:x-mailer :mime-version:content-type:content-transfer-encoding; b=ODAXL5Gqu3029SXoKgf5OiBddkA+UuBGfV1eMAq+q8k6FcxmN/BInzAxAys+ej2BWD rmJWQ+LqxGfipm1qjMxTBfSCwm+RmBmaClxiQCZlp1ymjhN92lUxnRHc5gF8rLiRxomI Hn8I44Hf21nNELoBOzB7tbPUL7edXbrSDNmAs=

On Wed, 8 Jun 2011 23:50:56 +0000
frank maltman
<frank.maltman AT googlemail.com>
wrote:

> Hello.
>
> Does anyone have a proof of 1 < two_power_pos p?

Got there in the end...

Lemma Z_1_le_two_power_pos_p : forall (p : positive),
  1 <= two_power_pos p.
Proof.
  intro p.
  assert (0 < 2) as H_obvious_02.
    reflexivity.
  assert (0 <= 0 <= Zpos p) as H_obvious_00p.
    auto with zarith.
  rewrite two_power_pos_correct.
  apply (Zpower_le_monotone 2 0 (Zpos p) H_obvious_02  H_obvious_00p).
Qed.

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