apply general (a + b) a b ha hb (le_refl _)
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
ha : 0 < a
hb : 0 < b
general :
  ∀ (n c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' p hp (c * d) (_ : c * d > 0) = nat_valuation_aux' p hp c hc + nat_valuation_aux' p hp d hd
⊢ nat_valuation_aux' p hp (a * b) (_ : a * b > 0) = nat_valuation_aux' p hp a ha + nat_valuation_aux' p hp b hb
no goals