theorem Legendre.hasLegendrePrime_one_to_five {n : ℕ} (hn1 : 1 ≤ n) (hn5 : n ≤ 5) : HasLegendrePrime n

theorem Legendre.hasLegendrePrime_one_to_oneHundred {n : ℕ} (hn1 : 1 ≤ n) (hn100 : n ≤ 100) : HasLegendrePrime n

TODO: Replace this with a generated/certified bound extension.