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)