A list of practical projects that anyone can solve in any programming language

Taking 1 not to be prime is, none the less, pretty clearly better than the alternative. Here are a few examples of neat things that would break if we took 1 to be prime:

When p is prime Z/pZ -- i.e., "integers mod p" -- is a field, meaning a thing in which you can do +,-,*,/. This would be false if we allowed p=1, though admittedly there's a not-too-crazy way you could change the usual definition of "field" that would fix it.

The "fundamental theorem of arithmetic": Every positive integer is the product of primes and this product is unique up to rearrangement. This would be false if we took 1 to be prime, because you can always add or remove 1s from the factorization.

The famous Riemann zeta function (zeta(s) = sum over positive integers n of n^-s) has a representation as an infinite product: zeta(s) = product over prime p of (1-p^-s)^-1. For a little example of why this is nice, note that it provides an instant proof that there are infinitely many primes, because as s->1 zeta(s)->infinity, which would be impossible if that were a finite product. This would become nonsense if we allowed p=1 because one factor would then be 1/0.

Prime numbers all have exactly two divisors (1 and p). This would become false if we took 1 to be prime.

Given how simple a Turing Machine can be, I seriously doubt (without any proof) that coq is not able to recreate a TM.

I am not an expert but the explanation about Turing Machines I read was in GED and involved a simple tape and a slack handful of symbols and operations and some basic hand waving. If coq can't manage that then it is unlikely to be useful - which I doubt.