fact: Definition nprim sc := match sc with | Proof_certif n _ => n | Lucas_certif n _ => n | Pock_certif n _ _ _ => n | SPock_certif n _ _ => n | Ell_certif n _ _ _ _ _ _ => n end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod