A two step induction proof

Consider the following function:

Fixpoint div2 (n:nat) : nat :=
  match n with 
  | 0 => 0
  | 1 => 0
  | S (S p) => S (div2 p)
  end.

Define the function mod2 which returns the rest of division by two, the prove the following equality for all n:

 n = 2 * (div2 n) + mod2 n

Solution

Look at This file