Add some comments to RewriteModuloAssociativity.v

From Mike Shulman's suggestions