feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634)
feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634)

For any `n : ℕ`, `n.factorization 0 = 0` and `n.factorization 1 = 0`






leanprover-community/mathlib,leanprover-community/mathlib