page 1  1 
We want to prove
( M : Nat ) mod2((2 * M) + 1) = 1 .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. 
