add _wand lemmas for big-ops

These seem so fundamental, so even though they are not hard to prove I was somewhat surprised that they do not already exist.