proposition: Lemma Zdivide_Ndivide (a b : Z) : 0 <= a -> 0 <= b -> (a | b) <-> (Z.to_nat a | Z.to_nat b)%nat.
proof: Proof. intros pa pb. rewrite Ndivide_Zdivide. rewrite 2 Z2Nat.id; tauto. Qed.
imports: Coq(ZArith Znumtheory Lia Psatz) Coqtail(Nlittle_fermat Ztools)