proposition: Lemma pow_mod_pred_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n.
proof: Proof. unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto. destruct a as (q,p). simpl mkProd_pred. destruct (p ?= 1)%P; rewrite IHl; mauto; simpl. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod