prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1.

This instance is slower than the instance decidable_prime defined below, but has the advantage that it works in the kernel.

If you need to prove that a particular number is prime, in any case you should not use dec_trivial, but rather by norm_num, which is much faster.

Returns the smallest prime factor of n ≠ 1.

This instance is faster in the virtual machine than decidable_prime_1, but slower in the kernel.

If you need to prove that a particular number is prime, in any case you should not use dec_trivial, but rather by norm_num, which is much faster.

factors n is the prime factorization of n, listed in increasing order.

The type of prime numbers