proposition: Lemma psplit_prime: forall l (p: positive), (forall (q: positive * positive), List.In q l -> prime (fst q)) -> prime p -> (p | Zmullp l)%Z -> List.In p (snd (psplit l)).
proof: Proof. intros l; elim l. unfold Zmullp; simpl. intros p _ H1 H2. case H1. absurd (p <= 1). apply Zlt_not_le; case H1; auto. apply Zdivide_le; auto with zarith. intros (a1, n1) l1 Hrec p Hp Hp1 Hp2. rewrite Zmullp_cons in Hp2. rewrite Zpos_mult_morphism in Hp2. case (prime_mult _ Hp1 _ _ Hp2); intros H1. assert (Hap: prime a1). change a1 with (fst (a1, n1)); apply Hp; auto with datatypes. simpl; case n1; try intros p1; case psplit; intros p2 l2; simpl snd; left; assert (HH: Zpos a1 = p); try (injection HH; auto); symmetry; apply prime_div_Zpower_prime with (Zpos n1); auto with zarith; rewrite <- Ppow_correct; auto. assert (HH: List.In p (snd (psplit l1))). apply Hrec; auto with datatypes. generalize HH; simpl. case psplit; case n1; simpl snd; auto with datatypes. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod