proposition: Lemma primeb_prime (n : Z) : primeb n = true <-> prime n.
proof: Proof. rewrite <-prime_sqrt_spec. unfold prime_sqrt, primeb. rewrite andb_true_iff, Z.ltb_lt, forallb_forall. split; intros [hn h]; split; auto. - intros x bx xn. specialize (h x). rewrite in_Zseq in h. spec h by lia. rewrite negb_true_iff, Z.eqb_neq in h. apply h, Zdivide_mod, xn. - intros x bx%in_Zseq. rewrite negb_true_iff, Z.eqb_neq, Z.mod_divide. 2:lia. apply h. lia. Qed.
imports: Coq(ZArith Znumtheory Lia List Bool) Coqtail(Ztools Zpow)