p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ∣ m
rw [← pow_one p]
no goals
p k m : ℕ
hk : 1 ≤ k
hpk : p ^ k ∣ m
⊢ p ^ 1 ∣ m
exact pow_dvd_of_le_of_pow_dvd hk hpk