proposition: Theorem divides_pdiv : forall p q : nat, 0 < q -> divides q p -> snd (pdiv p q) = 0.
proof: Proof. intros p q H (q1, H1); generalize (pdiv_def p q H); case (pdiv p q); simpl in |- *. intros q2 r2 (H2, H3). apply (div_unic_r p q q2 q1); split; auto. rewrite H1; ring. Qed.
imports: Coq(ArithRing) Bertrand(Misc)