proposition: Lemma prime_Nprime (p : Z) : prime p <-> Nprime (Z.to_nat p).
proof: Proof. split; intros pp. - apply Nprime_prime. rewrite Z2Nat.id; auto. apply prime_ge_2 in pp; lia. - rewrite <-(Z2Nat.id p). now apply Nprime_prime. apply Nprime_ge_2 in pp. lia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)