case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b

case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
rcases eq_or_ne a 0 with (rfl | ha)
case inr.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
case inr
p a b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ a
ha : a ≠ 0
⊢ padicValNat p (a / b) = padicValNat p a - padicValNat p b
obtain ⟨k, rfl⟩ := h
case inr.intro.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
case inr.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
obtain ⟨hb, hk⟩ := mul_ne_zero_iff.mp ha
no goals
case inr.intro.intro
p b : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
ha : b * k ≠ 0
hb : b ≠ 0
hk : k ≠ 0
⊢ padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
rw [mul_comm, k.mul_div_cancel hb.bot_lt, padicValNat.mul hk hb, Nat.add_sub_cancel]
no goals
case inl
p b : ℕ
hp : Fact (Nat.Prime p)
h : b ∣ 0
⊢ padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
simp