I think this lemma is by @haidang, but it might also be by @lgaeher.
Maybe this should be an Instance? Not sure.
Instance