mathlib

b3b5e355 - chore(data/nat/prime): slightly golf proof of mem_factors (#12143)