[Agda] primes

[Ruben Henner Zilibowitz]

Hi,

I'm having some difficulty finding a type that expresses "m is a prime  
number".

Here is what I've got:

-- Prime m is inhabited iff m is a prime number or 0 or 1.
Prime : (m : ℕ) -> Set
Prime m = forall {i} -> i < m -> i Divides m -> i ≡ 1

The problem is that 0 and 1 shouldn't be prime numbers but under this  
definition they are. So far I haven't been able to figure out  
something better. Any suggestions would be great.

Regards,

Ruben