proposition: Lemma prime_mult : forall p:Z, prime p -> forall a b:Z, (p | a * b) -> (p | a) \/ (p | b).
proof: Proof. intro p; simple induction 1; intros ? ? a b ?. case (Zdivide_dec p a); intuition. right; apply Gauss with a; auto with zarith. Qed.
imports: ZArith_base ZArithRing Zcomplements Zdiv Wf_nat