proposition: Lemma Prime_prime (n: nat) : Prime n -> prime (Z.of_nat n).
proof: Proof. intros. unfold Prime in H. destruct H. constructor. + lia. + intros. destruct H1. unfold rel_prime. set (Z.gcd n0 (Z.of_nat n)) as W. assert (W <= n0)%Z. { pose proof (Z.gcd_divide_l n0 (Z.of_nat n)). apply Z.divide_pos_le in H3. auto. lia. } pose proof (Z.gcd_divide_r n0 (Z.of_nat n)). assert (divide (Z.to_nat W) n). { destruct H4. exists (Z.to_nat x). unfold W. pose proof (Z.gcd_nonneg n0 (Z.of_nat n)). nia. } apply H0 in H5. destruct H5. - assert (W = 1)%Z by lia. rewrite <- H6. apply Znumtheory.Zgcd_is_gcd. - lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow