The Coq mailing list

[Michel Levy <michel.levy1948 AT gmail.com>]

On 19/02/2015 16:12, Abhishek Anand wrote:

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/

Thank you really much for your answer.
But how did you find it ? I was looking at the "official doc" in
  https://coq.inria.fr/distrib/current/stdlib/Coq.Numbers.Natural.Peano.NPeano.html
and I don't find Nat.log2_pow2 on this page or in the web index of the standard library.

Sincerely yours.

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