theorem TwinPrime.hasTwinPrimeFrom_le_eleven {N : ℕ} (hN : N ≤ 11) : HasTwinPrimeFrom N

theorem TwinPrime.hasTwinPrimeUpTo_of_thirteen_le {N : ℕ} (hN : 13 ≤ N) : HasTwinPrimeUpTo N

theorem TwinPrime.hasTwinPrimeFrom_le_oneMillion {N : ℕ} (hN : N ≤ 1000000) : HasTwinPrimeFrom N

TODO: Replace with certified coverage for a substantially larger bound.