add proof for plus_swap using rewrite. good tactic, but how does it interact with induction? also paste in inductive definition of binary numbers for next time