mathlib

0e834dfe - chore(data/nat/multiplicity): simplify proof (#14103)