proposition: Lemma prime_divisors : forall p:Z, prime p -> forall a:Z, (a | p) -> a = -1 \/ a = 1 \/ a = p \/ a = - p.
proof: Proof. intros p; destruct 1 as [H H0]; intros a ?. assert (a = - p \/ - p < a < -1 \/ a = -1 \/ a = 0 \/ a = 1 \/ 1 < a < p \/ a = p). { assert (Z.abs a <= Z.abs p) as H2 by (apply Zdivide_bounds; [ assumption | now intros -> ]). revert H2. pattern (Z.abs a); apply Zabs_ind; pattern (Z.abs p); apply Zabs_ind; intros H2 H3 H4. - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]; try intuition. destruct (Zle_lt_or_eq _ _ (Z.ge_le _ _ H3)) as [H6 | H6]; try intuition. destruct (Zle_lt_or_eq _ _ (Zlt_le_succ _ _ H6)) as [H7 | H7]; intuition. - contradict H2; apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. - destruct (Zle_lt_or_eq _ _ H4) as [H5 | H5]. + destruct (Zle_lt_or_eq _ _ H3) as [H6 | H6]; try intuition. assert (H7 : a <= Z.pred 0) by (apply Z.lt_le_pred; auto). destruct (Zle_lt_or_eq _ _ H7) as [H8 | H8]; intuition. assert (- p < a < -1); try intuition. now apply Z.opp_lt_mono; rewrite Z.opp_involutive. + now left; rewrite <- H5, Z.opp_involutive. - contradict H2. apply Zlt_not_le; apply Z.lt_trans with (2 := H); red; auto. } intuition idtac. - match goal with [hyp : a < -1 |- _] => rename hyp into H4 end. absurd (rel_prime (- a) p). + intros [H1p H2p H3p]. assert (- a | - a) by auto with zarith. assert (- a | p) as H5 by auto with zarith. apply H3p, Z.divide_1_r in H5; auto with zarith. destruct H5 as [H5|H5]. * contradict H4; rewrite <- (Z.opp_involutive a), H5 . apply Z.lt_irrefl. * contradict H4; rewrite <- (Z.opp_involutive a), H5 . discriminate. + apply H0; split. * now apply Z.opp_le_mono; rewrite Z.opp_involutive; apply Z.lt_le_incl. * now apply Z.opp_lt_mono; rewrite Z.opp_involutive. - match goal with [hyp : a = 0 |- _] => rename hyp into H2 end. contradict H. replace p with 0; try discriminate. now apply sym_equal, Z.divide_0_l; rewrite <-H2. - match goal with [hyp : 1 < a |- _] => rename hyp into H3 end. absurd (rel_prime a p). + intros [H1p H2p H3p]. assert (a | a) by auto with zarith. assert (a | p) as H5 by auto with zarith. apply H3p, Z.divide_1_r in H5; auto with zarith. destruct H5 as [H5|H5]. * contradict H3; rewrite <- (Z.opp_involutive a), H5 . apply Z.lt_irrefl. * contradict H3; rewrite <- (Z.opp_involutive a), H5 . discriminate. + apply H0; split; auto. now apply Z.lt_le_incl. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat