Add lemmas and max for Qp

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.

The library 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.