Thanks you two for you help! The final solution looks like this:

```
From mathcomp Require Import all_ssreflect prime zmodp reals.
Module Type Primes.
Variable n : nat.
Definition P := [set x : 'I_n.+1 | prime x].
Lemma four_notin_P : inZp 4 \notin P.
Proof.
Admitted.
End Primes.
```

Jannik Mähn has marked this topic as resolved.

@Jannik Mähn I was going to point to the coq-prima package, but now I see there are actually a number of packages defining them: https://github.com/thery/coqprime

https://coq.inria.fr/coq-package-index (search prime-numbers).

Thanks Bas, I'll have a look there as well!

Dear math-comp users, I have to reopen the topic.

How can we define a type for the set of primes that we have defined above?

So, given this definition:

```
From mathcomp Require Import all_ssreflect prime zmodp reals.
Module Type Primes.
Variable n : nat.
Definition P := [set x : 'I_n.+1 | prime x].
End Primes.
```

We need to write something like this:

```
From mathcomp Require Import all_ssreflect prime zmodp reals.
Module Type Primes.
Variable n : nat.
Definition P' : {set x : 'I_n.+1 | prime x} := [set x : 'I_n.+1 | prime x].
End Primes.
```

Where I get a syntax error right now.

There might also be another approach, where we define things like this:

```
From mathcomp Require Import all_ssreflect prime zmodp reals.
Module Type Primes.
Variable n : nat.
Definition P : {set 'I_n.+1} := [set : 'I_n.+1].
Parameter all_prime : forall x, x \in P -> prime x.
Definition Z_n_prod := [finType of P].
End Primes.
```

I want to define it in this

`finType`

notation becauce of the setting we're working in. Here I get the following error:

```
**Error:** `The term "P" has type "{set 'I_n.+1}" while it is expected to have type "Type".`
```

Thanks a lot in advance!

Last updated: Jul 15 2024 at 20:02 UTC