# Division by bounded recursion

Using the definition of a division function by bounded recursion given
by the following text :

Require Export Arith.
Fixpoint bdiv_aux (b m n:nat) {struct b} : nat * nat :=
match b with
| O => (0, 0)
| S b' =>
match le_gt_dec n m with
| left H => match bdiv_aux b' (m - n) n with
| (q, r) => (S q, r)
end
| right H => (0, m)
end
end.

Prove the following property:

bdiv_aux_correct2 :
forall b m n:nat, m <= b -> 0 < n -> snd (bdiv_aux b m n) < n.

Going home
## Solution

Follow this link

Yves Bertot
Last modified: Tue May 13 22:13:20 MEST 2003