proposition: Lemma in_mkProd_prime_div_in : forall p:positive, prime p -> forall (l:dec_prime), (forall k, In k l -> prime (fst k)) -> Z.divide p (mkProd l) -> exists n,In (p, n) l.
proof: Proof. induction l;simpl mkProd; simpl In; mauto. intros _ H1; absurd (p <= 1). apply Zlt_not_le; apply Z.lt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Zdivide_le; auto with zarith. intros. case prime_mult with (2 := H1); auto with zarith; intros H2. exists (snd a);left. destruct a;simpl in *. assert (Zpos p = Zpos p0). rewrite (prime_div_Zpower_prime p1 p p0); mauto. apply (H0 (p0,p1));auto. inversion H3; auto. destruct IHl as (n,H3); mauto. exists n; auto. Qed.
imports: List ZArith Zorder ZCAux LucasLehmer Pocklington ZCmisc Pmod