defined binary natural type
Added a proof by induction
Merge branch 'ch1Exercises'