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.
