# 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

Going home

Pierre Castéran