Lemmas for Positive, Negative, etc. and _+_ and _*_ for rationals

[Taneb]

This is pulled out from my branch for real numbers

A discovered annoyance (bug?) is that *-monoˡ-≤-nonNeg corresponds to *-monoʳ-<-pos, not *-monoˡ-<-pos as one may expect. But I don't want to fix that in this PR

[jamesmckinna]

This is pulled out from my branch for real numbers

Looks good!

A discovered annoyance (bug?) is that *-monoˡ-≤-nonNeg corresponds to *-monoʳ-<-pos, not *-monoˡ-<-pos as one may expect. But I don't want to fix that in this PR

Yes, I think this is an(other) example of left/right being mixed up in the library, and at some point, we should rationalise (and correctly implement) our conventions. Cf. #1436 (comment) and #1579 etc.

See also #2193 ...

[jamesmckinna]

Two comments:

• it would be great to find a way to make even the arguments p, q themselves inferrable, but I suspect this isn't possible without quotation/indirection, because of the usual 'arithmetic operations can't infer their arguments' objection (but I still have the fantasy that one day we might overcome that)
• all the lemmas are in Data.Rational.Properties: is there any relationship with/need for, any (additional) ones in Data.Rational.Unnormalised.Properties? (I've never been quite clear about the division of labour between the two...)

[Taneb]

all the lemmas are in Data.Rational.Properties: is there any relationship with/need for, any (additional) ones in Data.Rational.Unnormalised.Properties? (I've never been quite clear about the division of labour between the two...)

I'll admit I didn't do that simply out of laziness. But looking at it now, I don't think in this case doing it that way would be helpful.