This MR adds some helper lemmas, which are good to have in prosa and will be needed later in the ELF RTA.