mathlib3

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

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.