Induction: Solved part (a) of binary_inverse.
Induction: Solved exercise binary_inverse, with the redefinition of binary numbers, and changes to the previous exercises. Solved exercise addnC_informal.
Induction: Solved exercise eqnn_informal.