proposition: Lemma primedivmult : forall p n m : nat, Prime p -> Divides p (n * m) -> Divides p n \/ Divides p m.
proof: Proof. intros. elim (prime_div_or_gcd1 p (Z_of_nat n)). left. rewrite <- (abs_inj p). rewrite <- (abs_inj n). apply zdivdiv. assumption. right. rewrite <- (abs_inj p). rewrite <- (abs_inj m). apply zdivdiv. apply divmultgcd with (Z_of_nat n). elim H. intros. apply Zgt_neq. change (Z_of_nat p > Z_of_nat 0)%Z in |- *. apply Znat.inj_gt. apply gt_trans with 1. assumption. unfold gt in |- *. unfold lt in |- *. apply le_n. rewrite <- Znat.inj_mult. apply divzdiv. rewrite abs_inj. rewrite abs_inj. assumption. assumption. assumption. Qed.
imports: Arith ZArith Wf_nat lemmas natZ dec list exp divides prime modulo gcd