proposition: Lemma snd_all_pow_mod : forall n l (prod a :N), a mod (Zpos n) = a -> Z_of_N (snd (all_pow_mod prod a l n)) = (a^(mkProd' l)) mod n.
proof: Proof. induction l; simpl all_pow_mod; simpl mkProd';intros; mauto. destruct a as (q,p). rewrite IHl; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod