proposition: Lemma iter_pow_mod_spec : forall q p a, [|a|] = ([|a|] mod [|b|])%Z -> ([|iter_pos _ (fun x => pow x q) a p|] = [|a|]^q^p mod [|b|])%Z.
proof: Proof. intros q1 p1; elim p1; simpl iter_pos; clear p1. intros p1 Rec a Ha. rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]). repeat rewrite Rec. 2, 4: auto with zarith. match goal with |- (Zpower_pos ?X ?Y mod ?Z = _)%Z => apply trans_equal with (X ^ Y mod Z)%Z; auto end. rewrite <- Zpower_mod by auto with zmisc. rewrite <- Zpower_mult by auto with zmisc. rewrite <- Zpower_mod by auto with zmisc. rewrite <- Zpower_mult by auto with zarith zmisc. eq_tac; auto. eq_tac; auto. rewrite Zpos_xI. assert (tmp: forall x, (2 * x = x + x)%Z) by auto with zarith; rewrite tmp; clear tmp. repeat rewrite Zpower_exp by auto with zarith. rewrite Zpower_1_r; try ring; auto with misc. rewrite Zmod_mod; auto with zarith. rewrite Rec. rewrite Zmod_mod. reflexivity. rewrite Rec by auto with zmisc. rewrite Zmod_mod; auto with zarith. intros p1 Rec a Ha. repeat rewrite Rec. 2, 4: auto with zarith. rewrite <- Zpower_mod by auto with zmisc. rewrite <- Zpower_mult by auto with zmisc. eq_tac; auto. eq_tac; auto. rewrite Zpos_xO. assert (tmp: forall x, (2 * x = x + x)%Z) by auto with zarith; rewrite tmp; clear tmp. repeat rewrite Zpower_exp; auto with zarith. rewrite Zmod_mod; auto with zarith. intros a Ha; rewrite Zpower_1_r. rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); 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