induction n using caseStrongRecOnOddPrimes with
| zero => simp
| two => simp
| not_prime n hp hi =>
  specialize hi n
  simp at hi
  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]
| odd_prime n hp hi =>
  simp
  conv => rhs; rw [two_mul, pow_add]
  specialize hi n.succ _
  . cases n with
    | zero => contradiction  | succ n => linarith
  simp at hi
  rw [prodPrimesSplit (by linarith : n.succ ≤ (2*n).succ)]
  apply Nat.mul_le_mul hi
  apply le_trans _ chooseHalfLePowFour
  exact prodPrimesIocLeChoose
n : ℕ
⊢ prodPrimes n ≤ 4 ^ Nat.pred n
no goals