mathlib3

927b4685 - chore(data/nat/factorization/basic): golf pow_succ_factorization_not_dvd, remove import (#14936)

chore(data/nat/factorization/basic): golf pow_succ_factorization_not_dvd, remove import (#14936) Move `pow_succ_factorization_not_dvd` below `factorization_le_iff_dvd` and use this to golf it, eliminating the need for `tactic.linarith`