The Nth primes

@[simp]

theorem Nat.nth_prime_zero_eq_two : nth Prime 0 = 2

@[simp]

theorem Nat.nth_prime_one_eq_three : nth Prime 1 = 3

@[simp]

theorem Nat.nth_prime_two_eq_five : nth Prime 2 = 5

@[simp]

theorem Nat.nth_prime_three_eq_seven : nth Prime 3 = 7

@[simp]

theorem Nat.nth_prime_four_eq_eleven : nth Prime 4 = 11