p > 1 \ n dvd p)"
by (auto simp add: prime_nat_code)
lemmas prime_nat_simp_numeral [simp] = prime_nat_simp [of "numeral m"] for m
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
text{* A bit of regression testing: *}
lemma "prime(97::nat)" by simp
lemma "prime(997::nat)" by eval
lemma prime_imp_power_coprime_nat: "prime p \