Fundamental theorem of arithmetic

[Alizter]

We should prove the fundamental theorem of arithmetic for nat and IsPrime. The basic statement says that any given nat has a factorisation and any two factorisations are unique up to a permutation of factors. There is also a generalisation to unique factorisation domains with a possible semiring variant.

Another way to modify the statement for nat is to force uniqueness by enforcing an order of the prime factors of a given factorisation. Then the fundamental theorem of arithmetic essentially says that the type of factorisations of a nat is contractible.

In our calculations in homotopy theory, it's not apparent how useful this theorem actually is given that we can always manually factor a concrete number. So I wouldn't say this issue is a top priority.

One place to draw inspiration from is the following: https://github.com/coq-contribs/fundamental-arithmetics/blob/master/primes.v

[Alizter]

I've managed to prove the existence of factorizations, however the proof does not compute efficiently. This means you cannot do say Eval cbv in ... to see what the factorisation should be. This leaves the following concrete things to do in the future for this issue:

• Show that any two factorizations are unique up to permutation of prime factors.
• Show that the type of factorisations ordered by <= are contractible.
• Give a more efficient factorisation algorithm so we can compute concrete cases.