proposition: Theorem pdiv_not_divides : forall n m : nat, 0 < m -> snd (pdiv n m) <> 0 -> ~ divides m n.
proof: Proof. intros n m H H0; red in |- *; intros H1; case H0; apply divides_pdiv; auto. Qed.
imports: Coq(ArithRing) Bertrand(Misc)