Example primality certificates

Demonstrates pock%, pock3, and prime_cert% on primes up to 100+ digits, including the Ed25519 base point order and the Goldilocks prime 2^448 - 2^224 - 1.

Helpful links:

• https://www.alpertron.com.ar/ECM.HTM (integer factorisation calculator using elliptic curves)

theorem PrimeCert.prime_16290860017' : Nat.Prime 16290860017

theorem PrimeCert.prime_236684654874665389773181956283167565443541280517430278333971 : Nat.Prime 236684654874665389773181956283167565443541280517430278333971

theorem PrimeCert.prime_25519' : Nat.Prime (2 ^ 255 - 19)

theorem PrimeCert.prime_25519'' : Nat.Prime (2 ^ 255 - 19)

theorem PrimeCert.prime_448_224_1 : Nat.Prime (2 ^ 448 - 2 ^ 224 - 1)

theorem PrimeCert.prime_448_224_1' : Nat.Prime (2 ^ 448 - 2 ^ 224 - 1)

theorem PrimeCert.prime_ed25519_order : Nat.Prime (2 ^ 252 + 27742317777372353535851937790883648493)