fact: Fixpoint pow (a p:positive) {struct p} : positive := match p with | xH => a | xO p' =>let z := pow a p' in square z | xI p' => let z := pow a p' in square z * a end.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod