proposition: Theorem pdiv_def : forall m n : nat, 0 < n -> match pdiv m n with | (q, r) => m = q * n + r /\ r < n end.
proof: Proof. intros m n H; unfold pdiv in |- *; apply pdiv_aux_def with (p := m); auto with arith. Qed.
imports: Coq(ArithRing) Bertrand(Misc)