论文标题
原始测试和主要证书
Primality Tests and Prime Certificate
论文作者
论文摘要
本说明介绍了在Lucas-Lehmer测试和Pocklington证书的COQ中进行的正式化。它们都是Fermat Little定理的直接后果。 Fermat Little定理是使用基本组理论，尤其是Lagrange定理证明的。
This note presents a formalisation done in Coq of Lucas-Lehmer test and Pocklington certificate for prime numbers. They both are direct consequences of Fermat little theorem. Fermat little theorem is proved using elementary group theory and in particular Lagrange theorem.
