. cases n with
  | zero => contradiction  | succ n => linarith
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : ∀ (x : ℕ), x ≤ 2 * n → prodPrimes x ≤ 4 ^ Nat.pred x
⊢ Nat.succ n ≤ 2 * n

case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n
case odd_prime
n : ℕ
hp : Nat.Prime (Nat.succ (2 * n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
⊢ prodPrimes (Nat.succ (2 * n)) ≤ 4 ^ n * 4 ^ n