add version of Qp_lower_bound that returns less-than facts

Mainly, this has the advantage of showing up when doing SearchAbout (_ < _)%Qc.

Possibly this lemma could be generalized to work with all Qc, not just Qp, but then we couldn't reuse the existing Qp_lower_bound.