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.

Solution