fact: Hypothesis div_it_fix_eqn : forall (n m : nat) (h : 0 < m), div_it n m h = match le_gt_dec m n with left H => let (q, r) := div_it (n - m) m h in (S q, r) | right H => (0, n) end.
imports: Arith ArithRing Wf_nat