theorem eq_pow_prime_of_unit_of_congruent {K : Type u_1} {p : ℕ+} [Field K] (u : { x // x ∈ NumberField.ringOfIntegers K }ˣ) (hcong : ∃ n, ↑↑p ∣ ↑u - ↑n) : ∃ v, u = v ^ ↑p