proposition: Lemma Ndivide_Zdivide (a b : nat) : (a | b)%nat <-> (Z.of_nat a | Z.of_nat b).
proof: Proof. split; intros (k & e). - exists (Z.of_nat k). subst. lia. - destruct (Nat.eq_dec a 0). + assert (b = 0)%nat as -> by lia. apply Ndiv_0. + exists (Z.to_nat k). nia. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)