case inl
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0

case inr
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case inl
p n : ℕ
hp : Fact (Nat.Prime p)
⊢ p ^ n ∣ 0 ↔ 0 = 0 ∨ n ≤ padicValNat p 0
exact iff_of_true (dvd_zero _) (Or.inl rfl)
no goals
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
a : ℕ
ha : a ≠ 0
⊢ p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
rw [padicValNat_dvd_iff_le ha, or_iff_right ha]