Merge pull request #1 from fniksic/ssr

A few changes to Basics.v
a little better proof for addnA'