proposition: Theorem pdiv_divides : forall n m : nat, 0 < m -> snd (pdiv n m) = 0 -> divides m n.
proof: Proof. intros n m H; generalize (pdiv_def n m H); case (pdiv n m); simpl in |- *. intros n1 m1 (H1, H2) H3; exists n1; rewrite H1; rewrite H3; rewrite <- plus_n_O; auto. Qed.
imports: Coq(ArithRing) Bertrand(Misc)