proposition: Theorem not_divides_pdiv : forall p q : nat, 0 < q -> ~ divides q p -> snd (pdiv p q) <> 0.
proof: Proof. intros p q H; generalize (pdiv_def p q H); case (pdiv p q); simpl in |- *. intros q1 r1 (H1, H2) H3; red in |- *; intros H4; case H3; exists q1; rewrite H1; rewrite H4; ring. Qed.
imports: Coq(ArithRing) Bertrand(Misc)