Highest prime power dividing a nat?

Stream: Is there code for X?

[Eric Rodriguez]

is there any better way to get some prime power dividing a nat than:

let mf := (k+2).min_fac,
let pow := nat.log mf (nat.gcd (mf ^ (k+2)) (k+2)),

I'm dealing with Sort* so would rather avoid some and some_spec, but if it's the easiest that's fine too

[Kevin Buzzard]

Do you just mean padic_val_nat?

[Kevin Buzzard]

Ines was writing some API for it recently. I think this function deserves more love!

[Eric Rodriguez]

woo, that's amazing timing!