proposition: Lemma prime_sqrt_spec n : prime_sqrt n <-> prime n.
proof: Proof. rewrite <-prime_alt. symmetry. unfold prime', prime_sqrt. split; intros [bn h]; split; auto; intros x bx. - apply h. split. lia. pose proof Z.sqrt_lt_lin n; lia. - intros (y, e). destruct (Z_le_gt_dec x y) as [ xy | xy ]. + apply (h x); [ | exists y; lia ]. assert (1 < x). enough (x <> 0) by nia. intros ->. lia. split; auto. apply Z.sqrt_le_square; try lia. rewrite e. nia. + apply (h y); [ | exists x; lia ]. assert (1 < y). enough (y <> 0) by nia. intros ->. lia. split; auto. apply Z.sqrt_le_square; try lia. rewrite e. nia. Qed.
imports: Coq(ZArith Znumtheory Lia List Bool) Coqtail(Ztools Zpow)