prove p is prime for various prime order fields, useful for ECDH and EDDSA

[david415]

We have several cases of apologizing to the Lean compiler for not supplying proof of primality for some rather large primes:

def p : ℕ := 2^255 - 19
def basepoint : ZMod p := 9
def keySize : ℕ := 32

theorem p_is_prime : Nat.Prime p := by sorry
instance fact_p_is_prime : Fact (Nat.Prime p) := ⟨p_is_prime⟩
instance : Field (ZMod p) := ZMod.instField p

I'm told there exist various coqprime proofs for such things already. coqprime makes Pocklington certificates of primality:

https://github.com/thery/CoqPrime

https://github.com/mit-plv/fiat-crypto/blob/master/src/Spec/Curve25519.v#L16-L34

However someone from the Lean community has at least a partially working tactic for generating Pratt certificates of primality:

https://github.com/leanprover-community/mathlib4/blob/6439ce3f194a2acd309af6831d753e560c46bcf6/Mathlib/NumberTheory/LucasPrimality.lean#L567

According to one Lean community member: "you should probably manually create a Pratt certificate for your prime"