add a lemma I think will be needed