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