proposition: Lemma mkProd_pred_mkProd : forall l, (mkProd_pred l)*(mkProd' l) = mkProd l.
proof: Proof. induction l;simpl;intros; autorewrite with zmisc. reflexivity. generalize (pos_eq_1_spec (snd a)); destruct (snd a ?= 1)%P;intros. rewrite H. autorewrite with zmisc. replace (mkProd_pred l * (fst a * mkProd' l)) with (fst a *(mkProd_pred l * mkProd' l));try ring. rewrite IHl; mauto. rewrite Zmult_assoc. rewrite times_Zmult. rewrite (Zmult_comm (pow (fst a) (Pos.pred (snd a)) * mkProd_pred l)). rewrite Zmult_assoc. rewrite pow_Zpower. rewrite <-Ppred_Zminus;trivial. rewrite <- Zpower_Zsucc. replace (Z.succ (snd a - 1)) with ((snd a - 1)+1). replace ((snd a - 1)+1) with (Zpos (snd a)) by mauto. rewrite <- IHl. repeat rewrite Zmult_assoc. mauto. destruct (snd a - 1);trivial. assert (1 < snd a); auto with zarith. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod