proposition: Lemma prime_Prime (n: nat) : prime (Z.of_nat n) -> Prime n.
proof: Proof. intro. inversion H. clear H. unfold Prime. split. + lia. + intros. destruct H. assert (Z.of_nat n = Z.of_nat q * Z.of_nat x)%Z by lia. assert (n = 0 \/ 0 < n) by lia. destruct H3. - lia. - assert (1 < q < n \/ q = 1 \/ n <= q) by nia. destruct H4 as [H4 | [H4 | H4]]. * assert (1 <= Z.of_nat q < Z.of_nat n)%Z by lia. pose proof (H1 _ H5). subst. exfalso. assert (1 < x) by nia. unfold rel_prime in H6. inversion H6. assert (Z.of_nat q | Z.of_nat q). { exists 1%Z. auto. lia. } assert (Z.of_nat q | Z.of_nat (q * x))%Z. { exists (Z.of_nat x). lia. } pose proof (H9 _ H10 H11). destruct H12. destruct x0; nia. * left. auto. * right. destruct x; nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow