Add Qp lemmas

Adds a two additional lemmas for Qp.

Also renames a few lemmas that accidentally had Qc in their name instead of Qp. These where introduced back in !179 (merged) so it's probably safe to assume that no one are using the misnamed ones.