Rewrite a nat lit as product of prime factors?

Stream: Is there code for X?

[Thomas Murrills]

I'm wondering if there's e.g. a simproc_decl (or something else) for rewriting a natural number as a product of its prime factors. This would turn e.g. 24 into 2 * 2 * 2 * 3 or 2 ^ 3 * 3. I'm aware of Nat.factors (and Nat.prod_factors which should help in providing the proof of equality), but I'm wondering if someone has already written the thing which directly transforms literals! :)

[Damiano Testa]

I don't think that I have seen it, but I do think that it would be useful to have! When I needed some factorisation I was essentially going on variations of rw [show x = fac of x by norm_num], writing by hand fac of x!