simp only [Nat.pred_succ] at *
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ Nat.pred (Nat.succ (Nat.succ n))
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ (Nat.succ n)) ≤ 4 ^ (n + 1)