proposition: Lemma L_Euclides1 : forall p a b : nat, prime p -> divides p (a * b) -> ~ divides p a -> divides p b.
proof: Proof. intros; apply L_Euclides with a; auto. apply is_gcd_sym. apply prime_gcd; auto. Qed.
imports: Coq(Arith ArithRing Peano_dec Wf_nat)