Support rewriting with `Qp` inequalities
When doing Qp
reasoning I sometimes would have found it useful to use rewrite
to exploit inequalities. It would be nice to wire up Qp
's ≤
with setoid-based rewriting.
When doing Qp
reasoning I sometimes would have found it useful to use rewrite
to exploit inequalities. It would be nice to wire up Qp
's ≤
with setoid-based rewriting.