adding my solutions written up so far

Basics: complete.
Induction: all except the hardest exercise:
`Theorem bin_of_nat_normalized_sound: forall (b:bin), bin_of_nat(nat_of_bin b) = bin_normalize b.`