fact: Fixpoint pdiv_aux (m n p : nat) {struct p} : nat * nat := match ominus m n with | None => (0, m) | Some m1 => match p with | O => (m, n) | S p1 => match pdiv_aux m1 n p1 with | (q, r) => (S q, r) end end end.
imports: Coq(ArithRing) Bertrand(Misc)