mathlib

fa6b16e1 - feat(data/nat/prime): add nat.eq_two_pow_or_exists_odd_prime_and_dvd (#12395)