proposition: Theorem div_it_correct2: forall (m n : nat) (h : 0 < n), (snd (div_it m n h) < n).
proof: Proof. intros m; induction m as [m' Hrec] using (well_founded_ind lt_wf). intros n h; rewrite div_it_fix_eqn. case (le_gt_dec n m'); intros H. + assert (Hlt: m'-n < m') by auto with arith. generalize (Hrec (m'- n) Hlt n h); case (div_it (m'-n) n h); simpl; auto. + simpl; auto. Qed.
imports: Arith ArithRing Wf_nat