feat(data/nat/prime): factors of non-prime powers (#11546)
Adds the result `pow_factors_to_finset`, fills in `factors_mul_to_finset_of_coprime` for the sake of completion, and adjusts statements to take `ne_zero` rather than pos assumptions.
Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
