apply le_trans hi
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.succ n
case not_prime.succ
n : ℕ
hp : ¬Nat.Prime (Nat.succ (Nat.succ n))
hi : prodPrimes (Nat.succ n) ≤ 4 ^ n
⊢ 4 ^ n ≤ 4 ^ Nat.succ n