Skip to content

add version of Qp_lower_bound that returns less-than facts

Ralf Jung requested to merge ralf/lower-bound-lt into master

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.

Merge request reports