case inl
p : ℕ
⊢ p ^ padicValNat p 0 ∣ 0

case inr
p n : ℕ
hn : n > 0
⊢ p ^ padicValNat p n ∣ n
p n : ℕ
⊢ p ^ padicValNat p n ∣ n
rcases n.eq_zero_or_pos with (rfl | hn)
case inr.inl
n : ℕ
hn : n > 0
⊢ 1 ^ padicValNat 1 n ∣ n

case inr.inr
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ^ padicValNat p n ∣ n
case inr
p n : ℕ
hn : n > 0
⊢ p ^ padicValNat p n ∣ n
rcases eq_or_ne p 1 with (rfl | hp)
no goals
case inr.inr
p n : ℕ
hn : n > 0
hp : p ≠ 1
⊢ p ^ padicValNat p n ∣ n
rw [multiplicity.pow_dvd_iff_le_multiplicity, padicValNat_def'] <;> assumption
no goals
case inl
p : ℕ
⊢ p ^ padicValNat p 0 ∣ 0
simp
no goals
case inr.inl
n : ℕ
hn : n > 0
⊢ 1 ^ padicValNat 1 n ∣ n
simp