proposition: Lemma pow_mod_pred_spec : forall l a, ([|a|] = [|a|] mod [|b|] -> [|pow_mod_pred a l|] = [|a|]^(mkProd_pred l) mod [|b|])%Z.
proof: Proof. intros l; elim l; simpl pow_mod_pred; simpl mkProd_pred; clear l. intros; rewrite Zpower_1_r; auto with zarith. intros (p1,q1) l Rec a H; simpl snd; simpl fst. case (q1 ?= 1)%P; auto with zarith. rewrite Rec; auto. rewrite iter_pow_mod_spec; auto with zarith. rewrite times_Zmult; rewrite pow_Zpower. rewrite <- Zpower_mod; auto with zarith. rewrite Zpower_mult; auto with zarith. rewrite Zmod_small; auto with zarith. rewrite iter_pow_mod_spec; auto with zarith. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) Pmod Mod_op W Lucas PocklingtonCertificat NEll