fact: Definition div_it_F (f:nat->nat->nat*nat)(m n:nat) := match le_gt_dec n m with | left _ => let (q, r) := f (m-n) n in (S q, r) | right _ => (0, m) end.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9