This is a useful lemma (at least for me), and I don't think it's directly derivable from the other two _inv lemmas.
_inv