Make Qp operations reduce on constants
It would be nice if (1/2 + 1/2 = 1)%Qp
were definitionally true, by changing the computational behavior of Qp constants and addition.
We started discussing this in !188 (merged), for example starting at this comment: !188 (comment 57439)