Basics.v: Finish binary number exercise, including Inductive proof of distributivity