add useful-looking lemmas

(I'm using them in not-yet-checkedin code, but not in a
way that makes my proofs beautiful, sadly.)