Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Thomas,

On 10/04/2012 14:02, Thomas Sibut-Pinote wrote:
> Lemma dvdn_leq_log p m n : 0 < n -> m %| n -> logn p m <= logn p n
> 
> in the library prime.v, could be written in a stronger form:
> 
> Lemma dvdn_leq_log m n : 0 < n -> (m %| n <-> forall p, logn p m <= logn p 
> n).
>
> I would think one needs the right-to-left implication more often than the 
> other
> in arithmetic. At least, I need this for a theorem I am trying to prove.

While I do not use this library very much, I guess that the current way of 
going
the other way around, would be using dvdn_partP and then p_part to link (logn 
p
n) to n`_p.


> By the way, I think a theorem on the valuation of prime numbers in 
> factorial n
> would be a great addition to the library.

I think you're right.

Best,
-- 
Cyril