no goals
p a b✝ : ℕ
hp : Fact (Nat.Prime p)
m : ℕ
cpm : coprime p m
b : ℕ
dvd : m ∣ b
⊢ padicValNat p (b / m) = padicValNat p b
rw [padicValNat.div_of_dvd dvd, eq_zero_of_not_dvd (hp.out.coprime_iff_not_dvd.mp cpm),
  Nat.sub_zero]