proposition: Theorem 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.
proof: Proof. intros n m h; unfold div_it; case (div_it_terminates n m h). intros v Hex1; case (div_it_terminates (n-m) m h). intros v' Hex2; elim Hex2; elim Hex1; intros p Heq1 p' Heq2. rewrite <- Heq1 with (k := S (S (max p p')))(g := fun x y:nat => v). - rewrite <- Heq2 with (k := S (max p p'))(g := fun x y:nat => v). reflexivity. eauto with arith. - eauto with arith. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure chap9