page 1  1 
We want to prove
( M : Nat ) div2(2 * M) = M .We use induction on M to prove this goal. For this, we use the induction scheme based on the signature { 0, s } for Nat. Induction requires that we do the following:
And thus the main goal is proved. 
