# A companion theorem for division specified by a fixpoint equation

The following script contains the assumptions that describe a division
function. For instance, these facts can be obtained when the function is
defined using a *recursion by iteration technique*.

Parameter div_it : forall n m:nat, 0 < m -> nat*nat.
Axiom 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.

These assumptions can be used to prove a companion theorem:

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.
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 (le_plus_minus n m'); 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.

Prove the second companion theorem, with the following statement:

forall (m n:nat)(h:0 < n), snd (div_it m n h) < n

## Solution

Follow this link

Going home

Yves Bertot
Last modified: Tue May 20 15:26:16 MEST 2003