p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ ↑p ^ padicValInt p a ∣ a
rw [padicValInt_dvd_iff]
no goals
p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
exact Or.inr le_rfl