coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.

From: michel levy <michel.levy1948 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it.
Date: Thu, 19 Feb 2015 15:09:24 +0100

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

[Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., michel levy, 02/19/2015
- Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
  - Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Michel Levy, 02/19/2015
    - Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Abhishek Anand, 02/19/2015
      - Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Jean-Francois Monin, 02/19/2015
        
        Re: [Coq-Club] library Coq.Numbers.Natural.Abstract.NPow : how to use it., Robbert Krebbers, 02/19/2015