cases Nat.eq_zero_or_pos ((c + 1) * (d + 1) % p) with
| inl h =>
  have hh : (c + 1) % p = 0 ∨ (d + 1) % p = 0 := sorry
  cases hh with
  | inl h' =>
    subst hq
    rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
    have sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n := by
      apply Nat.le_of_lt_succ
      apply lt_of_lt_of_le _ h_sum
      apply Nat.add_lt_add_right
      apply Nat.div_lt_self _ prime.one_lt
      rw [Nat.add_comm]
      apply Nat.lt_add_right 0 1 c (Nat.lt_succ_self 0)
    rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
    rw [← ih ((c + 1) / (q + 2)) (d + 1) sorry sorry sum_le_n]
    have hey := nat_mul_div_assoc' (b := d+1) h'
    simp only [hey.symm, mul_s_s.symm]
    apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
  | inr h' =>
    subst hq
    rw [nat_valuation_aux'_of_dvd _ _ _ _ h']
    have sum_le_n : (c + 1) + (d + 1) / (q + 2) ≤ n := by
      apply Nat.le_of_lt_succ
      apply lt_of_lt_of_le _ h_sum
      apply Nat.add_lt_add_left
      apply Nat.div_lt_self _ prime.one_lt
      rw [Nat.add_comm]
      apply Nat.lt_add_right 0 1 d (Nat.lt_succ_self 0)
    rw [← add_assoc]
    rw [←ih (c + 1) ((d + 1) / (q + 2)) _ _ sum_le_n]
    have hey := nat_mul_div_assoc (a := c+1) h'
    simp only [hey.symm, mul_s_s.symm]
    apply nat_valuation_aux'_of_dvd (q+2) hp ((c+1) * (d+1)) _ h
| inr h =>
  have hc := ndiv_mul_left _ _ _ (ne_of_gt h)
  have hd := ndiv_mul_right _ _ _ (ne_of_gt h)
  simp [nat_valuation_aux'_of_not_dvd _ _ _ _ hc, nat_valuation_aux'_of_not_dvd _ _ _ _ hd]
  simp [←mul_s_s, nat_valuation_aux'_of_not_dvd _ _ _ _ (ne_of_gt h)]
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)
⊢ nat_valuation_aux' p (_ : 1 < p) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' p (_ : 1 < p) (Nat.succ c) hc + nat_valuation_aux' p (_ : 1 < p) (Nat.succ d) hd
no goals