proposition: Theorem div_it_correct1 : forall (m n:nat)(h:0 < n), m = fst (div_it m n h) * n + snd (div_it m n h).
proof: Proof. intros m; elim m using (well_founded_ind lt_wf). intros m' Hrec n h; rewrite div_it_fix_eqn. case (le_gt_dec n m'); intros H; trivial. pattern m' at 1; rewrite <- (Nat.sub_add n m'), Nat.add_comm; auto. pattern (m'-n) at 1. rewrite Hrec with (m'-n) n h; auto with arith. case (div_it (m'-n) n h); simpl; auto with arith. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9