fact: 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 | pair q r => (S q, r) end | right H => (0, m) end end.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure