proposition: Lemma Nprime_prime (p : nat) : Nprime p <-> prime (Z.of_nat p).
proof: Proof. rewrite <-prime_alt. split; intros (p1, Pp). - split. lia. intros n hn. specialize (Pp (Z.to_nat n) ltac:(lia)). rewrite Ndivide_Zdivide in Pp. rewrite Z2Nat.id in Pp. auto. lia. - split. lia. intros n hn. specialize (Pp (Z.of_nat n) ltac:(lia)). now rewrite Ndivide_Zdivide. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)