proposition: Lemma fst_all_pow_mod : forall (n a:positive) l (R:positive) (prod A :N), 1 < n -> Z_of_N prod = prod mod n -> Z_of_N A = a^R mod n -> Z_of_N (fst (all_pow_mod prod A l n)) = (fold_left (fun r (k:positive*positive) => (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n.
proof: Proof. induction l;simpl;intros; mauto. destruct a0 as (q,p);simpl. assert (Z_of_N A = A mod n). rewrite H1; mauto. rewrite (IHl (R * q)%positive); mauto; mauto. pattern (q * mkProd' l) at 2;rewrite (Zmult_comm q). repeat rewrite Zmult_assoc. rewrite Z_div_mult;auto with zmisc zarith. rewrite <- fold_aux. rewrite <- (fold_aux a (R * q * mkProd' l) n l (prod * (a ^ (R * mkProd' l) - 1)))... assert ( ((prod * (A ^ mkProd' l - 1)) mod n) = ((prod * ((a ^ R) ^ mkProd' l - 1)) mod n)). repeat rewrite (Zmult_mod prod);auto with zmisc. rewrite Zminus_mod;auto with zmisc. rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc. rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1; mauto. rewrite H3; mauto. rewrite H1; mauto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod