proposition: Lemma fold_pow_mod_spec : forall l (a:w), ([|a|] < [|b|])%Z -> [|fold_pow_mod a l|] = ([|a|]^(mkProd' l) mod [|b|])%Z.
proof: Proof. intros l; unfold fold_pow_mod; elim l; simpl fold_left; simpl mkProd'; auto; clear l. intros a H; rewrite Zpower_1_r; rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z a); auto with zarith. intros (p1, q1) l Rec a H. case (ZnZ.spec_to_Z a); auto with zarith; intros U1 U2. rewrite Rec. rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. rewrite <- Zpower_mod. rewrite times_Zmult; rewrite Zpower_mult; auto with zarith. apply Z.le_lt_trans with (2 := H); auto with zarith. rewrite Zmod_small; auto with zarith. rewrite m_op_spec.(power_mod_spec) with (t := [|a|]); auto with zarith. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. rewrite Zmod_small; auto with zarith. 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