(** * Pocklington's Criterion. * * @author Olga Caprotti and Martijn Oostdijk * @version $Revision$ *) Require Export Arith. Require Export ZArith. Require Export list. Require Export divides. Require Export mod. Require Export exp. Require Export gcd. Require Export prime. Require Export modprime. Require Export fermat. Require Export order. Require Export pock.