rw [add_assoc _ 1 _, add_comm 1, ← add_assoc]
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) + 1 +
      nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd
case inl.inl
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b : ℕ
ha : 0 < a
hb : 0 < b
n c : ℕ
hc : Nat.succ c > 0
d : ℕ
hd : Nat.succ d > 0
h_sum : Nat.succ c + Nat.succ d ≤ Nat.succ n
q : ℕ
mul_s_s : Nat.succ c * Nat.succ d = Nat.succ (c * d + c + d)
prime : Nat.Prime (q + 2)
hp : optParam (1 < q + 2) (_ : 1 < q + 2)
ih :
  ∀ (c d : ℕ) (hc : c > 0) (hd : d > 0),
    c + d ≤ n →
      nat_valuation_aux' (q + 2) hp (c * d) (_ : c * d > 0) =
        nat_valuation_aux' (q + 2) hp c hc + nat_valuation_aux' (q + 2) hp d hd
h : (c + 1) * (d + 1) % (q + 2) = 0
h' : (c + 1) % (q + 2) = 0
sum_le_n : (c + 1) / (q + 2) + (d + 1) ≤ n
⊢ nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ (c * d + c + d)) (_ : 0 < Nat.succ (c * d + c + d)) =
    nat_valuation_aux' (q + 2) (_ : 1 < q + 2) ((c + 1) / (q + 2)) (_ : 0 < (c + 1) / (q + 2)) +
        nat_valuation_aux' (q + 2) (_ : 1 < q + 2) (Nat.succ d) hd +
      1