specialize hi n
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : ∀ (x : ℕ), x ≤ n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : n ≤ n → prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)