n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (↑(factorization n) p + 1) ∣ n
⊢ False
n p : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ¬p ^ (↑(factorization n) p + 1) ∣ n
intro h
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : factorization (p ^ (↑(factorization n) p + 1)) ≤ factorization n
⊢ False
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (↑(factorization n) p + 1) ∣ n
⊢ False
rw [← factorization_le_iff_dvd (pow_pos hp.pos _).ne' hn] at h
no goals
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : factorization (p ^ (↑(factorization n) p + 1)) ≤ factorization n
⊢ False
simpa [hp.factorization] using h p