proposition: Lemma primedivmult : forall p n m : nat, Prime p -> divide p (n * m) -> divide p n \/ divide p m.
proof: Proof. intros. apply Prime_prime in H. assert (Z.divide (Z.of_nat p) (Z.of_nat n * Z.of_nat m)). { destruct H0. exists (Z.of_nat x). nia. } apply prime_mult in H1; auto. destruct H1. + left. destruct H1. exists (Z.to_nat x). nia. + right. destruct H1. exists (Z.to_nat x). nia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow