add proof for plus_swap. learned about assertions/nested proofs. this was actually a bit tricky