Add ltaddpr to iset.mm
Add ltaddpr to iset.mm

The proof is one that I came up with, rather than getting
from the literature. The result follows fairly directly from
arithmetic locatedness and our definition of <P .

metamath/set.mm,metamath/set.mm,metamath/set.mm