The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

It is already there in the standard library:

Require Export Coq.Numbers.Natural.Peano.NPeano.

SearchAbout (log2 (2^?x)).

(*

Nat.log2_pow2: forall a : nat, 0 <= a -> log2 (2 ^ a) = a

*)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Feb 19, 2015 at 9:09 AM, michel levy <michel.levy1948 AT gmail.com> wrote:

I want to prove some property of power like
  Lemma log2_power2 : forall x:nat, log2(2^x)=x.
It seems to me that I need the monotonicity properties written in Coq.Numbers.Natural.Abstract.NPow but
I don't know how to use these properties.
With  "Locate pow_l_r." I have the (sad) answer "No object of basename pow_l_r".

Can you help me ?

-- 
email : michel.levy AT imag.fr
http://membres-liglab.imag.fr/michel.levy