cases n with
| zero => simp
| succ n =>
  simp only [Nat.pred_succ] at *
  simp [prodPrimes]
  rw [primesSuccEqPrimesSelf hp, Nat.add_one]
  rw [← prodPrimes, Nat.add_one]
  apply le_trans hi
  simp [pow_succ]
case not_prime
n : ℕ
hp : ¬Nat.Prime (Nat.succ n)
hi : prodPrimes n ≤ 4 ^ Nat.pred n
⊢ prodPrimes (Nat.succ n) ≤ 4 ^ Nat.pred (Nat.succ n)
no goals