feat(data/nat/factorization): add lemma `factorization_le_iff_dvd` (#11377)
feat(data/nat/factorization): add lemma `factorization_le_iff_dvd` (#11377)

For non-zero `d n : ℕ`, `d.factorization ≤ n.factorization ↔ d ∣ n`





leanprover-community/mathlib,leanprover-community/mathlib