Add a few extra lemmas for
Qp and adds a
max operation for
Qp. The lemmas for
max are not exhaustive. The names of the lemmas are consistent with those in GenericMinMax.
GenericMinMax contains a way to implement
max (see for instance how it's used with
Q). I'm not sure if that's the better way to do it. But, modules aren't used in this way anywhere in stdpp so I opted to not use it.