chore(data/nat/factorization): Reorder lemmas and some minor golfing (#12144)

Some minor housework on this file, reordering and regrouping lemmas, adding and editing a few docstrings and section headers, and golfing a few proofs.

Author: stuart-presnell