Definition natdivrem (n m : nat) : dirprod nat nat. Proof. intros. induction n as [ | n IHn ]. - intros. apply (make_dirprod 0 0). - induction (natlthorgeh (S (pr2 IHn)) m). + apply (make_dirprod (pr1 IHn) (S (pr2 IHn))). + apply (make_dirprod (S (pr1 IHn)) 0). Defined.