proposition: Lemma fst_all_pow_mod : forall l (a:w) (R:positive) (prod A :w), [|prod|] = ([|prod|] mod [|b|])%Z -> [|A|] = ([|a|]^R mod [|b|])%Z -> [|fst (all_pow_mod prod A l)|] = ((fold_left (fun r (k:positive*positive) => (r * ([|a|] ^ (R* mkProd' l / (fst k)) - 1))) l [|prod|]) mod [|b|])%Z.
proof: Proof. intros l; elim l; simpl all_pow_mod; simpl fold_left; simpl fst; auto with zarith; clear l. intros (p1,q1) l Rec; simpl fst. intros a R prod A H1 H2. assert (F: (0 <= [|A|] < [|b|])%Z). rewrite H2. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. assert (F1: ((fun x => x = x mod [|b|])%Z [|fold_pow_mod A l|])). rewrite Zmod_small; auto. rewrite fold_pow_mod_spec; auto with zarith. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. assert (F2: ((fun x => x = x mod [|b|])%Z [|pred (fold_pow_mod A l)|])). rewrite Zmod_small; auto. rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); auto with zarith. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. rewrite (Rec a (R * p1)%positive); auto with zarith. rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); auto with zarith. rewrite(fun x => m_op_spec.(pred_mod_spec) x [|x|]); auto with zarith. rewrite fold_pow_mod_spec; auto with zarith. rewrite H2. repeat rewrite Zpos_mult. repeat rewrite times_Zmult. repeat rewrite <- Zmult_assoc. apply sym_equal; rewrite <- fold_aux; auto with zarith. apply sym_equal; rewrite <- fold_aux; auto with zarith. eq_tac; auto. match goal with |- context[fold_left ?x _ _] => apply f_equal2 with (f := fold_left x); auto with zarith end. rewrite Zmod_mod; auto with zarith. rewrite (Zmult_comm R); repeat rewrite <- Zmult_assoc; rewrite (Zmult_comm p1); rewrite Z_div_mult; auto with zarith. repeat rewrite (Zmult_mod [|prod|]);auto with zmisc. eq_tac; [idtac | eq_tac]; auto. eq_tac; auto. rewrite Zmod_mod; auto. repeat rewrite (fun x => Zminus_mod x 1); auto with zarith. eq_tac; auto; eq_tac; auto. rewrite Zmult_comm; rewrite <- Zpower_mod; auto with zmisc. rewrite Zpower_mult; auto with zarith. rewrite Zmod_mod; auto with zarith. rewrite Zmod_small; auto. rewrite(fun x y => m_op_spec.(mul_mod_spec) x y [|x|] [|y|]); auto with zarith. match goal with |- context[(?X mod ?Y)%Z] => case (Z_mod_lt X Y); auto with zarith end. rewrite(fun x => m_op_spec.(power_mod_spec) x [|x|]); auto with zarith. apply trans_equal with ([|A|] ^ p1 mod [|b|])%Z; auto. rewrite H2. rewrite Zpos_mult_morphism; rewrite Zpower_mult; auto with zarith. rewrite <- Zpower_mod; auto with zarith. rewrite Zmod_small; auto. 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