proposition: Theorem prime_alt p : prime' p <-> prime p.
proof: Proof. split; intros (Hp,H). - constructor; trivial; intros n Hn. constructor; auto with zarith; intros x Hxn Hxp. rewrite <- Z.divide_abs_l in Hxn, Hxp |- *. assert (Hx := Z.abs_nonneg x). set (y:=Z.abs x) in *; clearbody y; clear x; rename y into x. destruct (Z_0_1_more x Hx) as [->|[->|Hx']]. + exfalso. apply Z.divide_0_l in Hxn. absurd (1 <= n). * rewrite Hxn; red; auto. * intuition. + now exists 1. + elim (H x); auto. split; trivial. apply Z.le_lt_trans with n; try tauto. apply Z.divide_pos_le; auto with zarith. apply Z.lt_le_trans with (2 := proj1 Hn); red; auto. - constructor; trivial. intros n Hn Hnp. case (Zis_gcd_unique n p n 1). + constructor; auto with zarith. + apply H; auto with zarith. now intuition; apply Z.lt_le_incl. + intros H1; intuition; subst n; discriminate. + intros H1; intuition; subst n; discriminate. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat