simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
case inr
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
n : ℕ
ih :
  ∀ (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
c : ℕ
hc✝ : Nat.succ c > 0
d : ℕ
hd✝ : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
hq : q + 2 = p
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
h : (c + 1) * (d + 1) % p > 0
hc : (c + 1) % p ≠ 0
hd : (d + 1) % p ≠ 0
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) = 0
no goals