# On nested recursion

Complete the missing parts:
Require Import Arith.
Require Import Omega.
Fixpoint div2 (n:nat) : nat := match n with S (S p) => S (div2 p) | _ => 0 end.
(* as we advised in chapter 9, we use a specific induction principle
to reason on the division function. *)
Theorem div2_ind :
forall P:nat->Prop,
P 0 -> P 1 -> (forall n, P n -> P (S (S n))) ->
forall n, P n.
Proof.
intros.
assert (H' : P n /\ P (S n)).
elim n; intuition.
intuition.
Qed.
(* Once the induction principle breaks down the problem into the
various cases, the omega tactic can handle them. *)
Theorem double_div2_le : forall x:nat, div2 x + div2 x <= x.
Theorem f_lemma : forall x v, v <= div2 x -> div2 x + v <= x.

## Solution

This file

Going home

Yves Bertot
Last modified: Tue May 20 15:20:10 MEST 2003