proposition: Lemma L_Euclides2 : forall p a b : nat, prime p -> divides p (a * b) -> divides p a \/ divides p b.
proof: Proof. intros. elim (divides_dec p a); [ left | right ]; auto. apply L_Euclides1 with a; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)